Mathlib triage dashboard

Welcome to the PR triage page! This page is perfect if you intend to look for pull request which seem to have stalled.
Feedback on designing this page or further information to include is very welcome.

Quick links: PR statistics | Not yet landed PRs | Review status | Stale unassigned PRs | Stale assigned PRs | Likely-spurious CI failures | Tech debt PRs | PRs blocked on a zulip discussion | PRs with just a merge conflict | Stale new contributor PRs | PRs not into master | PRs with an 'approved' review | All open PRs | Other lists of PRs

Overall statistics

• 495 (25.0%) are awaiting review (these ones), among these 68 (13.5%) by new contributors (these ones)
• 295 (14.9%) are blocked on another PR
• 141 (7.1%) are awaiting the PR author's action
• 242 (12.2%) have a merge conflict: among these, 115 (47.5%) would be ready for review otherwise: these
• 33 (1.7%) are labelled help-wanted or please-adopt (roughly these)
• 741 (37.4%) are marked as draft or work in progress
• 10 (0.5%) are awaiting the outcome of a zulip discussion (these ones)
• 1 (0.1%) have contradictory labels (these ones)
• 20 (1.0%) are delegated (stale ones are here)
• 1 (0.1%) have been sent to bors (stale ones are here)

Approved, not yet landed PRs

• 0 PRs are ready to merge — among these no stale ones, congratulations!
• 34 PRs are waiting on maintainer approval (these), of which 25 have not been updated in a day (these)
• 34 PRs have been delegated and not updated in a day

  Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
  23600	mattrobball author:mattrobball	perf(Quiver.Basic): make `IsThin` a `class`	It seems problematic that `Quiver.IsThin` is an `abbrev` for (essentially) `Subsingleton`. We turn it in a one-field class. --- [](https://gitpod.io/from-referrer/)	delegated	27/21	Mathlib/CategoryTheory/Bicategory/Coherence.lean,Mathlib/CategoryTheory/Category/Preorder.lean,Mathlib/CategoryTheory/Generator/Basic.lean,Mathlib/CategoryTheory/Groupoid/Basic.lean,Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean,Mathlib/CategoryTheory/Limits/SmallComplete.lean,Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean,Mathlib/CategoryTheory/Skeletal.lean,Mathlib/CategoryTheory/Subobject/MonoOver.lean,Mathlib/CategoryTheory/Thin.lean,Mathlib/Combinatorics/Quiver/Basic.lean	11	16	['b-mehta', 'github-actions', 'leanprover-bot', 'mathlib-bors', 'mattrobball']	nobody	124-33992 4 months ago	139-32796 4 months ago	0-5717 1 hour
  23213	mattrobball author:mattrobball	chore(RingTheory.Derivation): add a `LinearMapClass` instance	Often we want `simp` to call `map_zero` or `map_add` for a `Derivation`. To find the `ZeroHomClass` or `AddHomClass` instance necessary it starts to climb up the type class hierarchy including looking for a `LinearMapClass` instance which didn't exist. Consequently, sythesis would look in a lot of crazy places trying to summon ring structures on the module or on derivations itself. Here we add the missing `LinearMapClass` instance so that `simp` is more efficient. --- [](https://gitpod.io/from-referrer/)	t-algebra delegated label:t-algebra$	5/3	Mathlib/RingTheory/Derivation/Basic.lean	1	8	['github-actions', 'j-loreaux', 'leanprover-bot', 'mathlib-bors', 'mattrobball']	nobody	104-11258 3 months ago	104-11258 3 months ago	47-39026 47 days
  23214	mattrobball author:mattrobball	perf(Module.LinearMap.Defs): deprioritize projections to parents for `SemilinearMapClass`	Trying to figure out if a given type has a `SemilinearMapClass` instance when all we want is an `AddHomClass` or a `MulActionSemiHomClass` can be quite expensive since there are multiple ways to crawl the algebraic hierarchy to generate `LinearMapClass` instances. If these fail, then they fail slowly. We deprioritize the projections from `SemilinearMapClass` to `AddHomClass` and `MulActionSemiHomClass` to make this one of the last choices. --- [](https://gitpod.io/from-referrer/)	t-algebra delegated label:t-algebra$	6/0	Mathlib/Algebra/Module/LinearMap/Defs.lean	1	6	['github-actions', 'j-loreaux', 'leanprover-bot', 'mathlib-bors', 'mattrobball']	nobody	104-11024 3 months ago	104-11024 3 months ago	47-32152 47 days
  23137	grunweg author:grunweg	chore(Topology): some more fun_prop tagging	--- [](https://gitpod.io/from-referrer/)	t-topology delegated	8/4	Mathlib/Dynamics/Flow.lean,Mathlib/Topology/Algebra/Monoid.lean	2	10	['github-actions', 'grunweg', 'j-loreaux', 'mathlib-bors']	nobody	103-13473 3 months ago	103-13473 3 months ago	34-32727 34 days
  25473	adomani author:adomani	feat(CI): check that Mathlib files have lean or md extension	Twice recently there have been files with an "intended" `.lean` extension in `Mathlib/`: * #24942, ending in `;lean`; * #25457, ending in `.Lean`. `mk_all` does not add these files to `Mathlib.lean`, since they do not end in `.lean` and this later causes problems. This CI step checks that all files in `Mathlib/` end with `.lean` or `.md`. See #25474 for a test where the new step [correctly fails](https://github.com/leanprover-community/mathlib4/actions/runs/15464097783/job/43532018379?pr=25474). --- [](https://gitpod.io/from-referrer/)	CI delegated	10/0	.github/workflows/lint_and_suggest_pr.yml	1	10	['adomani', 'bryangingechen', 'github-actions', 'grunweg', 'mathlib-bors']	nobody	76-45047 2 months ago	76-45937 2 months ago	0-11212 3 hours
  18693	Ruben-VandeVelde author:Ruben-VandeVelde	feat: add ConjRootClass	Co-authored-by: FR --- From #6718 [](https://gitpod.io/from-referrer/)	new-contributor t-algebra delegated label:t-algebra$	213/0	Mathlib.lean,Mathlib/FieldTheory/Minpoly/ConjRootClass.lean,Mathlib/FieldTheory/Minpoly/IsConjRoot.lean	3	16	['LessnessRandomness', 'Vierkantor', 'alreadydone', 'github-actions', 'grunweg', 'mathlib-bors']	Vierkantor assignee:Vierkantor	75-62607 2 months ago	86-38160 2 months ago	94-8480 94 days
  23240	urkud author:urkud	feat(Topology/Maps): `IsOpenMap` and `ClusterPt`	--- [](https://gitpod.io/from-referrer/)	t-topology delegated	17/4	Mathlib/Topology/Maps/Basic.lean	1	8	['eric-wieser', 'github-actions', 'grunweg', 'mathlib-bors', 'urkud']	nobody	75-39969 2 months ago	150-8950 4 months ago	0-12104 3 hours
  25765	JovanGerb author:JovanGerb	feat(gcongr): lemma for rewriting inside divisibility	TODO: add test to show that we can rewrite using `a ≡ b [ZMOD n]` inside `n ∣ 2 * a + 1`. edit: it's not yet entirely clear if this is the right thing to do. --- [](https://gitpod.io/from-referrer/)	t-data delegated	5/0	Mathlib/Data/Int/ModEq.lean	1	3	['fpvandoorn', 'github-actions', 'mathlib-bors']	nobody	68-3484 2 months ago	68-39022 2 months ago	1-19951 1 day
  22366	kim-em author:kim-em	feat: `check_equalities` tactic for diagnosing defeq problems	The `check_equalities` tactic, which checks the typing of equalities in the goal, reporting discrepancies between the implicit type argument of the equality, and the inferred types of the left and right hand sides, at "instances and reducible" transparency. Reports from this tactic do not necessarily indicate a problem, although typically `simp` should reduce rather than increase the reported discrepancies. `check_equalities` may be useful in diagnosing uses of `erw`.	t-meta delegated	118/3	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Basic.lean,Mathlib/Tactic/CategoryTheory/CheckCompositions.lean,Mathlib/Tactic/CheckEqualities.lean,Mathlib/Tactic/Common.lean,MathlibTest/check_equalities.lean	7	16	['adomani', 'b-mehta', 'eric-wieser', 'github-actions', 'grunweg', 'kim-em', 'mathlib-bors']	nobody	19-44291 19 days ago	159-36860 5 months ago	15-14325 15 days
  25481	kbuzzard author:kbuzzard	chore: refactor Algebra.TensorProduct.rightAlgebra	The declaration `Algebra.TensorProduct.rightAlgebra` makes `A ⊗[R] B` into a `B`-algebra (here `R` is a `CommSemiring`, `A` is a `Semiring` and an `R`-algebra, and `B` is a `CommSemiring` and an `R`-algebra). It is not an instance because if A = B it causes a diamond. However in the many cases where A isn't B, it can occasionally be useful. However one could imagine that in the many cases where an R-module `M` also isn't `B`, it might occasionally be useful to make `M ⊗[R] B` into a `B`-module (and indeed I am finding this in FLT). With the current definition of `Algebra.TensorProduct.rightAlgebra` this is difficult to do without causing diamonds in the case when `M` happens to be an `R`-algebra (by which I mean "I failed to do this in finite time"). One fix for this is just to redefine `Algebra.TensorProduct.rightAlgebra` so that the `smul` field is ``` smul b ab := TensorProduct.comm _ _ _ (b • (TensorProduct.comm _ _ _ ab)) ``` i.e. literally "swap the product around, use mathlib's instance making `B ⊗[R] A` into a `B`-algebra, and then swap back". Then the same definition can be used to make `M ⊗[R] B` into a `B`-module and on the odd occasion where this point of view is useful, there is no diamond. This is what we do in this PR. After adding one simp lemma there is no breakage at all in mathlib. Furthermore, for those who have observed that we want to build on this algebra instance sometimes and, for example, add instances of the form "if M is finite over R then M ⊗[R] B is finite over B" -- these instances are really easy to add now with this new definition, because you simply pull back the analogous finite left module instance along the isomorphism M ⊗[R] B = B ⊗[R] M. Examples (from FLT, where the right action is put in a scope): ``` scoped instance [Module.Finite R M] : Module.Finite A (M ⊗[R] A) := Module.Finite.equiv (Module.TensorProduct.comm R A M) scoped instance [Module.Free R M] : Module.Free A (M ⊗[R] A) := Module.Free.of_equiv (Module.TensorProduct.comm R A M) ``` --- [](https://gitpod.io/from-referrer/)	t-algebra delegated label:t-algebra$	33/6	Mathlib/RingTheory/TensorProduct/Basic.lean	1	7	['adomani', 'github-actions', 'kbuzzard', 'leanprover-bot', 'mathlib-bors']	adomani assignee:adomani	19-36484 19 days ago	19-43613 19 days ago	56-85445 56 days
  23669	erdOne author:erdOne	feat(FieldTheory): abelian extensions	--- [](https://gitpod.io/from-referrer/)	t-algebra delegated label:t-algebra$	74/0	Mathlib.lean,Mathlib/FieldTheory/Galois/Abelian.lean,Mathlib/NumberTheory/Cyclotomic/Gal.lean	3	16	['acmepjz', 'alreadydone', 'chrisflav', 'erdOne', 'github-actions', 'mathlib-bors', 'riccardobrasca', 'xroblot']	riccardobrasca assignee:riccardobrasca	14-44468 14 days ago	43-48708 1 month ago	29-68817 29 days
  27872	JovanGerb author:JovanGerb	chore(gcongr): clean up imports	This PR removes redundant `gcongr` imports. And when we do import `gcongr`, we now also import the core `@[gcongr]` tags, and also `grw`. --- [](https://gitpod.io/from-referrer/)	large-import delegated	7/23	Archive/Imo/Imo2019Q4.lean,Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean,Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean,Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean,Mathlib/Algebra/Order/BigOperators/Expect.lean,Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Chebyshev.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Convex/Star.lean,Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean,Mathlib/Combinatorics/Enumerative/Catalan.lean,Mathlib/Combinatorics/SetFamily/FourFunctions.lean,Mathlib/Combinatorics/SimpleGraph/Density.lean,Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/NumberTheory/FLT/Polynomial.lean,Mathlib/NumberTheory/FermatPsp.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Filter/AtTopBot/Archimedean.lean,Mathlib/Tactic/GCongr/CoreAttrs.lean,Mathlib/Topology/EMetricSpace/Paracompact.lean	21	10	['JovanGerb', 'bryangingechen', 'github-actions', 'grunweg', 'mathlib-bors']	nobody	14-13495 14 days ago	14-13495 14 days ago	4-34325 4 days
  27018	Komyyy author:Komyyy	feat: Finite product of Alexandrov-discrete spaces is Alexandrov-discrete	--- - [x] depends on: #27016 [](https://gitpod.io/from-referrer/)	t-topology delegated	93/9	Mathlib/Data/Set/Lattice.lean,Mathlib/Data/Set/Lattice/Image.lean,Mathlib/Order/Filter/Ker.lean,Mathlib/Topology/AlexandrovDiscrete.lean,Mathlib/Topology/NhdsKer.lean	5	8	['github-actions', 'mathlib-bors', 'mathlib4-dependent-issues-bot', 'ocfnash']	ocfnash assignee:ocfnash	13-57856 13 days ago	13-57856 13 days ago	10-20441 10 days
  28260	euprunin author:euprunin	chore(Analysis/Fourier): golf entire `fourier_zero` and `fourier_zero'` using `simp`	--- Show trace profiling of fourier_zero ### Trace profiling of `fourier_zero` before PR 28260 ```diff diff --git a/Mathlib/Analysis/Fourier/AddCircle.lean b/Mathlib/Analysis/Fourier/AddCircle.lean index 6238f58476..99dbb05621 100644 --- a/Mathlib/Analysis/Fourier/AddCircle.lean +++ b/Mathlib/Analysis/Fourier/AddCircle.lean @@ -126,2 +126,3 @@ theorem fourier_coe_apply' {n : ℤ} {x : ℝ} : -- simp normal form is `fourier_zero'` +set_option trace.profiler true in theorem fourier_zero {x : AddCircle T} : fourier 0 x = 1 := by ``` ``` ℹ [2482/2482] Built Mathlib.Analysis.Fourier.AddCircle info: Mathlib/Analysis/Fourier/AddCircle.lean:128:0: [Elab.async] [0.066690] elaborating proof of fourier_zero [Elab.definition.value] [0.066228] fourier_zero [Elab.step] [0.065930] induction x using QuotientAddGroup.induction_on simp only [fourier_coe_apply] norm_num [Elab.step] [0.065922] induction x using QuotientAddGroup.induction_on simp only [fourier_coe_apply] norm_num [Elab.step] [0.055636] simp only [fourier_coe_apply] Build completed successfully. ``` ### Trace profiling of `fourier_zero` after PR 28260 ```diff diff --git a/Mathlib/Analysis/Fourier/AddCircle.lean b/Mathlib/Analysis/Fourier/AddCircle.lean index 6238f58476..0542519008 100644 --- a/Mathlib/Analysis/Fourier/AddCircle.lean +++ b/Mathlib/Analysis/Fourier/AddCircle.lean @@ -126,10 +126,8 @@ theorem fourier_coe_apply' {n : ℤ} {x : ℝ} : -- simp normal form is `fourier_zero'` +set_option trace.profiler true in theorem fourier_zero {x : AddCircle T} : fourier 0 x = 1 := by - induction x using QuotientAddGroup.induction_on - simp only [fourier_coe_apply] - norm_num + simp -theorem fourier_zero' {x : AddCircle T} : @toCircle T 0 = (1 : ℂ) := by - have : fourier 0 x = @toCircle T 0 := by rw [fourier_apply, zero_smul] - rw [← this]; exact fourier_zero +theorem fourier_zero' : @toCircle T 0 = (1 : ℂ) := by + simp ``` ``` ℹ [2482/2482] Built Mathlib.Analysis.Fourier.AddCircle info: Mathlib/Analysis/Fourier/AddCircle.lean:128:0: [Elab.async] [0.041217] elaborating proof of fourier_zero [Elab.definition.value] [0.040843] fourier_zero [Elab.step] [0.040316] simp [Elab.step] [0.040305] simp [Elab.step] [0.040291] simp [Meta.isDefEq] [0.013042] ✅️ 0 • ?m =?= 0 • x [Meta.isDefEq] [0.010734] ✅️ instHSMul =?= instHSMul [Meta.isDefEq.delta] [0.010705] ✅️ instHSMul =?= instHSMul [Meta.synthInstance] [0.010613] ✅️ SMulWithZero ℤ (AddCircle T) [Meta.synthInstance] [0.010175] ✅️ apply @AddGroup.intSMulWithZero to SMulWithZero ℤ (AddCircle T) [Meta.synthInstance.tryResolve] [0.010141] ✅️ SMulWithZero ℤ (AddCircle T) ≟ SMulWithZero ℤ (AddCircle T) [Meta.isDefEq] [0.010882] ❌️ ↑1 =?= ↑1 Build completed successfully. ``` --- Show trace profiling of fourier_zero' ### Trace profiling of `fourier_zero'` before PR 28260 ```diff diff --git a/Mathlib/Analysis/Fourier/AddCircle.lean b/Mathlib/Analysis/Fourier/AddCircle.lean index 6238f58476..c97c6382dd 100644 --- a/Mathlib/Analysis/Fourier/AddCircle.lean +++ b/Mathlib/Analysis/Fourier/AddCircle.lean @@ -131,2 +131,3 @@ theorem fourier_zero {x : AddCircle T} : fourier 0 x = 1 := by +set_option trace.profiler true in theorem fourier_zero' {x : AddCircle T} : @toCircle T 0 = (1 : ℂ) := by ``` ``` ℹ [2482/2482] Built Mathlib.Analysis.Fourier.AddCircle info: Mathlib/Analysis/Fourier/AddCircle.lean:133:0: [Elab.command] [0.040228] theorem fourier_zero' {x : AddCircle T} : @toCircle T 0 = (1 : ℂ) := by have : fourier 0 x = @toCircle T 0 := by rw [fourier_apply, zero_smul] rw [← this]; exact fourier_zero [Elab.definition.header] [0.039678] fourier_zero' [Elab.step] [0.039292] expected type: Sort ?u.10460, term @toCircle T 0 = (1 : ℂ) [Elab.step] [0.039281] expected type: Sort ?u.10460, term binrel% Eq✝ (@toCircle T 0) (1 : ℂ) [Meta.synthInstance] [0.023079] ❌️ CoeT ℂ x Circle info: Mathlib/Analysis/Fourier/AddCircle.lean:133:0: [Elab.async] [0.050645] elaborating proof of fourier_zero' [Elab.definition.value] [0.049639] fourier_zero' [Elab.step] [0.049079] have : fourier 0 x = @toCircle T 0 := by rw [fourier_apply, zero_smul] rw [← this]; exact fourier_zero [Elab.step] [0.049067] have : fourier 0 x = @toCircle T 0 := by rw [fourier_apply, zero_smul] rw [← this]; exact fourier_zero [Elab.step] [0.047714] have : fourier 0 x = @toCircle T 0 := by rw [fourier_apply, zero_smul] [Elab.step] [0.047690] focus refine no_implicit_lambda% (have : fourier 0 x = @toCircle T 0 := ?body✝; ?_) case body✝ => with_annotate_state"by" (rw [fourier_apply, zero_smul]) [Elab.step] [0.047680] refine no_implicit_lambda% (have : fourier 0 x = @toCircle T 0 := ?body✝; ?_) case body✝ => with_annotate_state"by" (rw [fourier_apply, zero_smul]) [Elab.step] [0.047675] refine no_implicit_lambda% (have : fourier 0 x = @toCircle T 0 := ?body✝; ?_) case body✝ => with_annotate_state"by" (rw [fourier_apply, zero_smul]) [Elab.step] [0.016566] refine no_implicit_lambda% (have : fourier 0 x = @toCircle T 0 := ?body✝; ?_) [Elab.step] [0.016520] expected type: ↑(toCircle 0) = 1, term no_implicit_lambda% (have : fourier 0 x = @toCircle T 0 := ?body✝; ?_) [Elab.step] [0.016512] expected type: ↑(toCircle 0) = 1, term (have : fourier 0 x = @toCircle T 0 := ?body✝; ?_) [Elab.step] [0.016502] expected type: ↑(toCircle 0) = 1, term have : fourier 0 x = @toCircle T 0 := ?body✝; ?_ [Elab.step] [0.016409] expected type: Sort ?u.12245, term fourier 0 x = @toCircle T 0 [Elab.step] [0.016398] expected type: Sort ?u.12245, term binrel% Eq✝ (fourier 0 x) (@toCircle T 0) [Elab.step] [0.031091] case body✝ => with_annotate_state"by" (rw [fourier_apply, zero_smul]) [Elab.step] [0.031024] with_annotate_state"by" (rw [fourier_apply, zero_smul]) [Elab.step] [0.031018] with_annotate_state"by" (rw [fourier_apply, zero_smul]) [Elab.step] [0.031012] with_annotate_state"by" (rw [fourier_apply, zero_smul]) [Elab.step] [0.031006] (rw [fourier_apply, zero_smul]) [Elab.step] [0.031000] rw [fourier_apply, zero_smul] [Elab.step] [0.030995] rw [fourier_apply, zero_smul] [Elab.step] [0.030987] rw [fourier_apply, zero_smul] [Elab.step] [0.030977] (rewrite [fourier_apply, zero_smul]; with_annotate_state"]" (try (with_reducible rfl))) [Elab.step] [0.030972] rewrite [fourier_apply, zero_smul]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.030964] rewrite [fourier_apply, zero_smul]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.026599] rewrite [fourier_apply, zero_smul] [Meta.isDefEq] [0.016855] ✅️ 0 • x =?= 0 • ?m [Meta.isDefEq] [0.015512] ✅️ instHSMul =?= instHSMul [Meta.isDefEq.delta] [0.015494] ✅️ instHSMul =?= instHSMul [Meta.synthInstance] [0.015404] ✅️ SMulWithZero ℤ (AddCircle T) [Meta.synthInstance] [0.014948] ✅️ apply @AddGroup.intSMulWithZero to SMulWithZero ℤ (AddCircle T) [Meta.synthInstance.tryResolve] [0.014922] ✅️ SMulWithZero ℤ (AddCircle T) ≟ SMulWithZero ℤ (AddCircle T) [Meta.isDefEq] [0.014466] ✅️ SMulWithZero ℤ (AddCircle T) =?= SMulWithZero ℤ ?m.13159 [Meta.synthInstance] [0.010847] ✅️ Zero (AddCircle T) Build completed successfully. ``` ### Trace profiling of `fourier_zero'` after PR 28260 ```diff diff --git a/Mathlib/Analysis/Fourier/AddCircle.lean b/Mathlib/Analysis/Fourier/AddCircle.lean index 6238f58476..f13a398896 100644 --- a/Mathlib/Analysis/Fourier/AddCircle.lean +++ b/Mathlib/Analysis/Fourier/AddCircle.lean @@ -127,9 +127,7 @@ theorem fourier_coe_apply' {n : ℤ} {x : ℝ} : theorem fourier_zero {x : AddCircle T} : fourier 0 x = 1 := by - induction x using QuotientAddGroup.induction_on - simp only [fourier_coe_apply] - norm_num + simp -theorem fourier_zero' {x : AddCircle T} : @toCircle T 0 = (1 : ℂ) := by - have : fourier 0 x = @toCircle T 0 := by rw [fourier_apply, zero_smul] - rw [← this]; exact fourier_zero +set_option trace.profiler true in +theorem fourier_zero' : @toCircle T 0 = (1 : ℂ) := by + simp ``` ``` ℹ [2482/2482] Built Mathlib.Analysis.Fourier.AddCircle info: Mathlib/Analysis/Fourier/AddCircle.lean:131:0: [Elab.command] [0.045555] theorem fourier_zero' : @toCircle T 0 = (1 : ℂ) := by simp [Elab.definition.header] [0.044962] fourier_zero' [Elab.step] [0.044931] expected type: Sort ?u.10311, term @toCircle T 0 = (1 : ℂ) [Elab.step] [0.044920] expected type: Sort ?u.10311, term binrel% Eq✝ (@toCircle T 0) (1 : ℂ) [Meta.synthInstance] [0.031268] ❌️ CoeT ℂ x Circle info: Mathlib/Analysis/Fourier/AddCircle.lean:131:0: [Elab.async] [0.027859] elaborating proof of fourier_zero' [Elab.definition.value] [0.027542] fourier_zero' [Elab.step] [0.027179] simp [Elab.step] [0.027169] simp [Elab.step] [0.027156] simp [Meta.isDefEq] [0.011252] ❌️ ↑1 =?= ↑1 [Meta.isDefEq.delta] [0.010804] ❌️ ↑1 =?= ↑1 [Meta.isDefEq] [0.010774] ❌️ 1 =?= 1 [Meta.isDefEq] [0.010717] ❌️ { x // 0 ≤ x } =?= Circle [Meta.isDefEq] [0.010706] ❌️ { x // 0 ≤ x } =?= ↥(Submonoid.unitSphere ℂ) [Meta.isDefEq] [0.010684] ❌️ fun x ↦ 0 ≤ x =?= fun x ↦ x ∈ Submonoid.unitSphere ℂ [Meta.isDefEq] [0.010675] ❌️ 0 ≤ x =?= x ∈ Submonoid.unitSphere ℂ Build completed successfully. ``` --- [](https://gitpod.io/from-referrer/)	t-analysis delegated	3/6	Mathlib/Analysis/Fourier/AddCircle.lean	1	4	['eric-wieser', 'euprunin', 'github-actions', 'mathlib-bors']	nobody	9-5358 9 days ago	9-5358 9 days ago	0-15279 4 hours
  27180	ADedecker author:ADedecker	feat: quotient of a monoid with zero by a multiplicative congruence	--- My motivation is getting a more conceptual construction of [ValuativeRel.ValueGroupWithZero](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Valuation/ValuativeRel.html#ValuativeRel.ValueGroupWithZero), but I think this is of independent interest. [](https://gitpod.io/from-referrer/)	t-algebra delegated label:t-algebra$	141/26	Mathlib.lean,Mathlib/Data/Quot.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/GroupTheory/Congruence/GroupWithZero.lean	5	31	['ADedecker', 'eric-wieser', 'github-actions', 'mathlib-bors', 'ocfnash']	ocfnash assignee:ocfnash	7-45067 7 days ago	7-58275 7 days ago	28-12053 28 days
  27305	eric-wieser author:eric-wieser	feat: instances for `ZeroHom` and `OneHom`	This is motivated by wanting to write some lemmas about how the def in #27272 behaves on addition and scalar multiplcation, which requires these operations to first be defined. This shows that `ZeroHom` forms an `AddCommGroup` and `Module`, as well as analogous intermediate statements and `OneHom` results. --- - [x] depends on: #27318 [](https://gitpod.io/from-referrer/)	t-algebra delegated label:t-algebra$	187/0	Mathlib/Algebra/Group/Hom/Basic.lean,Mathlib/Algebra/Group/Hom/Instances.lean,Mathlib/Algebra/GroupWithZero/Action/Hom.lean,Mathlib/Algebra/Module/Hom.lean	4	7	['YaelDillies', 'adomani', 'eric-wieser', 'github-actions', 'mathlib-bors', 'mathlib4-dependent-issues-bot']	ericrbg assignee:ericrbg	6-35677 6 days ago	6-37724 6 days ago	21-65819 21 days
  27109	pechersky author:pechersky	feat(RingTheory/AdicValuation): valuation_surjective	for both the base valuation and the one on the extension --- [](https://gitpod.io/from-referrer/)	t-ring-theory t-analysis t-number-theory delegated	31/0	Mathlib/RingTheory/DedekindDomain/AdicValuation.lean,Mathlib/Topology/Algebra/Valued/ValuedField.lean	2	4	['github-actions', 'mathlib-bors', 'mathlib4-merge-conflict-bot', 'riccardobrasca']	riccardobrasca assignee:riccardobrasca	2-61049 2 days ago	2-61049 2 days ago	34-19371 34 days
  28366	BoltonBailey author:BoltonBailey	chore(downstream_dashboard.py): Allow empty workflow list	This PR allows the workflows list to be empty. When I try to run it on my repository with listing any workflows, I currently get the following error: ``` File "/Users/boltonbailey/Desktop/mathlibcontribution/mathlib4/scripts/downstream_dashboard.py", line 189, in check_workflow_uses_action workflow_filename = repo['workflows'][workflow_name] KeyError: 'workflows' During handling of the above exception, another exception occurred: Traceback (most recent call last): File "/Users/boltonbailey/Desktop/mathlibcontribution/mathlib4/scripts/downstream_dashboard.py", line 321, in main() File "/Users/boltonbailey/Desktop/mathlibcontribution/mathlib4/scripts/downstream_dashboard.py", line 260, in main success = check_workflow_uses_action(repo, 'build', 'leanprover/lean-action') and success File "/Users/boltonbailey/Desktop/mathlibcontribution/mathlib4/scripts/downstream_dashboard.py", line 193, in check_workflow_uses_action example_entry = {**repo, 'workflows': {**repo['workflows'], workflow_name: f'{workflow_name}.yml'}} KeyError: 'workflows' ``` It would be nice if I could run the script without specifying the workflows I already have in the `downstream_repos.yml` file. --- [](https://gitpod.io/from-referrer/)	CI delegated	5/2	scripts/downstream_dashboard.py	1	3	['Vierkantor', 'github-actions', 'mathlib-bors']	nobody	2-57442 2 days ago	2-57442 2 days ago	4-33511 4 days
  27958	pechersky author:pechersky	feat(NumberTheory/Padics): norm of Int lt one iff p divides	On the way to p-1 roots of unity With helper lemmas for natCast and simplification of norms of Int.natAbs Move some lemmas out of `padicNormE` namespace into `Padic` namespace which is similar to already existing lemmas in `PadicInt` namespace --- [](https://gitpod.io/from-referrer/)	t-algebra t-analysis t-number-theory delegated label:t-algebra$	92/38	Mathlib/Analysis/Normed/Ring/Basic.lean,Mathlib/NumberTheory/Harmonic/Int.lean,Mathlib/NumberTheory/Padics/Complex.lean,Mathlib/NumberTheory/Padics/Hensel.lean,Mathlib/NumberTheory/Padics/PadicIntegers.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/NumberTheory/Padics/RingHoms.lean	7	29	['YaelDillies', 'github-actions', 'kckennylau', 'mathlib-bors', 'pechersky', 'riccardobrasca']	YaelDillies assignee:YaelDillies	2-40176 2 days ago	2-45796 2 days ago	13-35113 13 days
  28446	mitchell-horner author:mitchell-horner	feat(Combinatorics/SimpleGraph): `card_edgeFinset_map`	--- Needed for a proof of the Erdős-Stone-Simonovits theorem in future PR. [](https://gitpod.io/from-referrer/)	t-combinatorics delegated	47/14	Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Finite.lean,Mathlib/Combinatorics/SimpleGraph/Maps.lean,Mathlib/Combinatorics/SimpleGraph/Operations.lean	4	10	['b-mehta', 'eric-wieser', 'github-actions', 'mathlib-bors', 'mitchell-horner']	nobody	1-48978 1 day ago	2-6293 2 days ago	4-6247 4 days
  27696	pechersky author:pechersky	feat(Padic/WithVal): WithVal v is isomorphic to Q_p as fields and uniform spaces	On the way to a topological ring equiv --- [](https://gitpod.io/from-referrer/)	t-algebra t-number-theory delegated label:t-algebra$	187/0	Mathlib.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/NumberTheory/Padics/WithVal.lean	3	13	['faenuccio', 'github-actions', 'mathlib-bors', 'riccardobrasca']	riccardobrasca assignee:riccardobrasca	1-29324 1 day ago	1-29324 1 day ago	19-78579 19 days
  28165	javra author:javra	feat(CategoryTheory/Enriched): transport enrichment on enriched ordinary categories	--- [](https://gitpod.io/from-referrer/)	infinity-cosmos t-category-theory delegated	147/3	Mathlib/CategoryTheory/Enriched/Basic.lean,Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean	2	6	['emilyriehl', 'github-actions']	b-mehta assignee:b-mehta	0-41764 11 hours ago	10-19472 10 days ago	10-24008 10 days
  28448	ShreckYe author:ShreckYe	chore(Data/Nat/Factorization/PrimePow): possibly simplify the last line of `isPrimePow_pow_iff`	Found this while working on #28557.	t-data new-contributor easy delegated	1/1	Mathlib/Data/Nat/Factorization/PrimePow.lean	1	2	['ShreckYe', 'github-actions']	nobody	0-30087 8 hours ago	3-29756 3 days ago	6-10855 6 days
  27174	ADedecker author:ADedecker	chore(OreLocalization): generalize some results from rings to monoids with zeros	--- My motivation is getting a more conceptual construction of [ValuativeRel.ValueGroupWithZero](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Valuation/ValuativeRel.html#ValuativeRel.ValueGroupWithZero), but I think this is of independent interest. [](https://gitpod.io/from-referrer/)	t-algebra delegated label:t-algebra$	112/73	Mathlib.lean,Mathlib/RingTheory/OreLocalization/Basic.lean,Mathlib/RingTheory/OreLocalization/NonZeroDivisors.lean,Mathlib/RingTheory/OreLocalization/Ring.lean	4	6	['Ruben-VandeVelde', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib-bors', 'riccardobrasca']	jcommelin assignee:jcommelin	0-20847 5 hours ago	2-59034 2 days ago	33-30654 33 days
  14712	FR-vdash-bot author:FR-vdash-bot	perf: change instance priority and order about `OfNat`	--- [](https://gitpod.io/from-referrer/)	slow-typeclass-synthesis t-algebra merge-conflict delegated label:t-algebra$	49/20	Mathlib/Algebra/Group/Nat.lean,Mathlib/Algebra/Group/ZeroOne.lean,Mathlib/Algebra/Homology/Embedding/Basic.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/Data/BitVec.lean,Mathlib/Data/Nat/Cast/Defs.lean,Mathlib/Data/Rat/Defs.lean,Mathlib/Data/UInt.lean,Mathlib/NumberTheory/ArithmeticFunction.lean	9	24	['FR-vdash-bot', 'MichaelStollBayreuth', 'eric-wieser', 'github-actions', 'j-loreaux', 'leanprover-bot', 'mathlib-bors']	nobody	318-53054 10 months ago	320-76530 10 months ago	20-15089 20 days
  19275	eric-wieser author:eric-wieser	fix: if nolint files change, do a full rebuild	Otherwise CI will succeed when removing entries from the file, but fail later when someone changes something unrelated. --- [](https://gitpod.io/from-referrer/)	merge-conflict delegated	8/0	lakefile.lean	1	20	['YaelDillies', 'adomani', 'eric-wieser', 'github-actions', 'grunweg', 'mathlib-bors']	nobody	138-39398 4 months ago	138-39398 4 months ago	0-214 3 minutes
  17129	joneugster author:joneugster	feat(Tactic/Linter): add unicode linter for unicode variant-selectors	Unicode characters can be followed by one of the two "variant-selectors" `\FE0E` (text) or `\FE0F` (emoji). These appear to the user as a single unicode character and they might copy them by accident. For example `✅️` (`\u2705\uFE0F`), `✅` (`\u2705`) and `✅︎` (`\u2705\uFE0E`) are three variants of the "same" unicode character. The one without variant-selector might display as either emoji or not, depending on the user's device and font. Add unicode linter ensuring variant-selector only appear on specified characters and also ensuring these characters always have the correct variant selector to avoid confusions. Everything flagged by this linter can be fixed fully automatically with `lake exe lint-style --fix` or by commenting `bot fix style` on the PR. --- - tracking PR: #16215 ## Zulip discussions: - https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Whitelist.20for.20Unicode.3F - https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20specific.20font ## Related PRs: - leanprover/lean4#5015 added some emoji-variant selectors to Emojis used in `Lean` itself. [](https://gitpod.io/from-referrer/)	large-import t-linter merge-conflict delegated awaiting-author	245/14	Mathlib.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/TextBased.lean,Mathlib/Tactic/Linter/UnicodeLinter.lean,Mathlib/Tactic/Widget/Calc.lean,Mathlib/Tactic/Widget/CongrM.lean,Mathlib/Tactic/Widget/Conv.lean,Mathlib/Tactic/Widget/GCongr.lean,Mathlib/Topology/ContinuousMap/Weierstrass.lean,MathlibTest/LintStyleTextBased.lean	11	25	['YaelDillies', 'adomani', 'github-actions', 'grunweg', 'joneugster', 'kim-em', 'leanprover-community-bot-assistant']	nobody	96-33420 3 months ago	96-33422 3 months ago	82-54712 82 days
  24409	urkud author:urkud	chore(*): fix `nmem` vs `not_mem` names	--- There are some missing/buggy deprecations, I'm going to fix them later today or tomorrow. [](https://gitpod.io/from-referrer/)	awaiting-zulip tech debt merge-conflict delegated awaiting-author	317/176	Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean,Mathlib/Algebra/Group/Indicator.lean,Mathlib/Algebra/Group/Support.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Order/Group/Indicator.lean,Mathlib/Algebra/Polynomial/AlgebraMap.lean,Mathlib/Algebra/Polynomial/Degree/Operations.lean,Mathlib/Analysis/Calculus/BumpFunction/Basic.lean,Mathlib/Analysis/Calculus/DSlope.lean,Mathlib/Analysis/Calculus/Deriv/Basic.lean,Mathlib/Analysis/Calculus/Deriv/Support.lean,Mathlib/Analysis/Calculus/FDeriv/Basic.lean,Mathlib/Analysis/Calculus/Rademacher.lean,Mathlib/Analysis/Complex/RemovableSingularity.lean,Mathlib/Analysis/Convex/Cone/InnerDual.lean,Mathlib/Analysis/Convex/Cone/Proper.lean,Mathlib/Analysis/Convolution.lean,Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean,Mathlib/Data/LocallyFinsupp.lean,Mathlib/Data/Set/Basic.lean,Mathlib/Data/Set/Insert.lean,Mathlib/Dynamics/Ergodic/Conservative.lean,Mathlib/Dynamics/Ergodic/Ergodic.lean,Mathlib/Dynamics/Ergodic/Function.lean,Mathlib/Dynamics/PeriodicPts/Defs.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/PartitionOfUnity.lean,Mathlib/GroupTheory/CosetCover.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/LinearAlgebra/FreeModule/PID.lean,Mathlib/LinearAlgebra/PID.lean,Mathlib/LinearAlgebra/RootSystem/Base.lean,Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean,Mathlib/MeasureTheory/Function/ContinuousMapDense.lean,Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean,Mathlib/MeasureTheory/Function/L2Space.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean,Mathlib/MeasureTheory/Integral/Average.lean,Mathlib/MeasureTheory/Integral/Bochner/Set.lean,Mathlib/MeasureTheory/Integral/Layercake.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean,Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean,Mathlib/MeasureTheory/Measure/AddContent.lean,Mathlib/MeasureTheory/Measure/DiracProba.lean,Mathlib/MeasureTheory/Measure/Haar/Unique.lean,Mathlib/MeasureTheory/Measure/Restrict.lean,Mathlib/MeasureTheory/Measure/WithDensity.lean,Mathlib/MeasureTheory/OuterMeasure/AE.lean,Mathlib/MeasureTheory/SetSemiring.lean,Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean,Mathlib/Order/Filter/Cocardinal.lean,Mathlib/Order/Filter/Cofinite.lean,Mathlib/Order/Filter/Tendsto.lean,Mathlib/Order/Filter/Ultrafilter/Basic.lean,Mathlib/Probability/Distributions/Uniform.lean,Mathlib/Probability/Kernel/Basic.lean,Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean,Mathlib/RingTheory/AdicCompletion/LocalRing.lean,Mathlib/RingTheory/Ideal/Maximal.lean,Mathlib/RingTheory/LaurentSeries.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean,Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean,Mathlib/RingTheory/Spectrum/Maximal/Localization.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,Mathlib/Topology/Algebra/InfiniteSum/Group.lean,Mathlib/Topology/Algebra/Module/Cardinality.lean,Mathlib/Topology/Algebra/Support.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean,Mathlib/Topology/Order/Basic.lean,Mathlib/Topology/UrysohnsLemma.lean	77	4	['b-mehta', 'github-actions', 'jcommelin', 'leanprover-community-bot-assistant', 'mathlib-bors']	nobody	79-68138 2 months ago	79-68138 2 months ago	0-55045 15 hours
  13483	adomani author:adomani	feat: automatically replace deprecations	This PR introduces `lake exe update_deprecations` that uses the cache to automatically replace deprecated declarations with the corresponding un-deprecated one. The script handles namespacing, replacing a possibly non-fully-qualified, deprecated name with the fully-qualified non-deprecated name. It is also possible to use ```bash lake exe update_deprecations --mods One.Two.Three,Dd.Ee.Ff ``` to limit the scope of the replacements to the modules `One.Two.Three` and `Dd.Ee.Ff`. This is intended to be a first step in automating updates: combining this with a linter that emits appropriate warnings, the functionality of `lake exe update_deprecations` can be extended to perform more complicated updates. --- [](https://gitpod.io/from-referrer/)	t-meta merge-conflict delegated awaiting-author	306/0	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/UpdateDeprecations.lean,MathlibTest/UpdateDeprecations.lean,lakefile.lean,scripts/README.md,scripts/update_deprecations.lean	7	16	['YaelDillies', 'adomani', 'github-actions', 'j-loreaux', 'jcommelin', 'leanprover-community-bot-assistant', 'mathlib-bors', 'sgouezel']	joneugster assignee:joneugster	71-309 2 months ago	71-310 2 months ago	34-82472 34 days
  17627	hrmacbeth author:hrmacbeth	feat: universal properties of vector bundle constructions	Characterizations for the smoothness of maps into the total spaces of (1) the direct sum of two vector bundles; (2) the pullback of a vector bundle. This gap in the library was exposed by #17358. --- - [x] depends on: #22804 [](https://gitpod.io/from-referrer/)	t-differential-geometry merge-conflict delegated	311/9	Mathlib/Data/Bundle.lean,Mathlib/Geometry/Manifold/VectorBundle/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/Pullback.lean,Mathlib/Topology/FiberBundle/Constructions.lean	4	24	['PatrickMassot', 'github-actions', 'grunweg', 'hrmacbeth', 'j-loreaux', 'leanprover-community-bot-assistant', 'mathlib-bors', 'mathlib4-dependent-issues-bot', 'sgouezel']	grunweg assignee:grunweg	46-77308 1 month ago	46-77308 1 month ago	91-73632 91 days
  26911	JovanGerb author:JovanGerb	chore: fix naming of `mono` and `monotone`	The naming convention says: "We use `_mono` for `a ≤ b → f a ≤ f b` and `_anti` for `a ≤ b → f b ≤ f a`, so we also use `_monotone` for `Monotone f`, `_antitone` for `Antitone f`, `_strictMono` for `StrictMono f`, `_strictAnti` for `StrictAnti f`, etc..." This PR swaps `mono`/`anti` and `monotone`/`antitone` where required so that `monotone` refers to `Monotone`, while `mono` refers to a lemma that might be tagged with `@[gcongr]` This PR does not address - `mul_left_monotone` and `mul_right_monotone` are exactly the wrong way around - `monotone_right`/`mono_right` vs `right_monotone`/`right_mono` - `monotone_arcsin` vs `arcsin_monotone` edit: TODO: `ideal_mono` and friends --- [](https://gitpod.io/from-referrer/)	merge-conflict delegated	238/171	Archive/Imo/Imo1962Q1.lean,Archive/Wiedijk100Theorems/AbelRuffini.lean,Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean,Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean,Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean,Mathlib/Algebra/Group/Pointwise/Set/Basic.lean,Mathlib/Algebra/Order/Field/Basic.lean,Mathlib/Algebra/Order/Group/Basic.lean,Mathlib/Algebra/Order/Group/Finset.lean,Mathlib/Algebra/Order/Group/PosPart.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean,Mathlib/Algebra/Order/ToIntervalMod.lean,Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean,Mathlib/Analysis/Analytic/Composition.lean,Mathlib/Analysis/Convex/Deriv.lean,Mathlib/Analysis/Normed/Order/UpperLower.lean,Mathlib/Analysis/PSeries.lean,Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean,Mathlib/Analysis/SpecificLimits/Basic.lean,Mathlib/Analysis/SpecificLimits/FloorPow.lean,Mathlib/Combinatorics/SetFamily/Kleitman.lean,Mathlib/Combinatorics/SimpleGraph/Girth.lean,Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean,Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean,Mathlib/Computability/Ackermann.lean,Mathlib/Data/ENNReal/Inv.lean,Mathlib/Data/ENNReal/Operations.lean,Mathlib/Data/Nat/Choose/Factorization.lean,Mathlib/Data/Real/Pi/Bounds.lean,Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean,Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean,Mathlib/MeasureTheory/Constructions/Polish/Basic.lean,Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean,Mathlib/MeasureTheory/OuterMeasure/Operations.lean,Mathlib/NumberTheory/Bertrand.lean,Mathlib/NumberTheory/FermatPsp.lean,Mathlib/NumberTheory/Padics/Hensel.lean,Mathlib/Order/Concept.lean,Mathlib/Order/Filter/AtTopBot/Defs.lean,Mathlib/Order/Fin/Basic.lean,Mathlib/Order/Heyting/Basic.lean,Mathlib/Order/Heyting/Boundary.lean,Mathlib/Order/Heyting/Regular.lean,Mathlib/Order/Hom/Set.lean,Mathlib/Order/Interval/Set/Fin.lean,Mathlib/Order/KrullDimension.lean,Mathlib/Order/UpperLower/Closure.lean,Mathlib/Probability/StrongLaw.lean,Mathlib/RingTheory/DedekindDomain/Different.lean,Mathlib/RingTheory/DedekindDomain/Ideal.lean,Mathlib/RingTheory/FractionalIdeal/Basic.lean,Mathlib/RingTheory/FractionalIdeal/Operations.lean,Mathlib/Topology/EMetricSpace/Lipschitz.lean,Mathlib/Topology/MetricSpace/Antilipschitz.lean,Mathlib/Topology/MetricSpace/Holder.lean	59	8	['JovanGerb', 'bryangingechen', 'github-actions', 'leanprover-community-bot-assistant', 'linesthatinterlace', 'mathlib-bors']	bryangingechen assignee:bryangingechen	39-85023 1 month ago	40-27647 1 month ago	2-60107 2 days
  25941	erdOne author:erdOne	feat(AlgebraicGeometry): inverse limits and schemes of finite type	We prove the following: Given a cofiltered diagram `D` of quasi-compact `S`-schemes with affine transition maps, and another scheme `X` of finite type over `S`. Then the canonical map `colim Homₛ(Dᵢ, X) ⟶ Homₛ(lim Dᵢ, X)` is injective. Co-authored-by: Christian Merten --- [](https://gitpod.io/from-referrer/)	large-import t-algebraic-geometry merge-conflict delegated	368/3	Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean,Mathlib/AlgebraicGeometry/Morphisms/Affine.lean,Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean,Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean,Mathlib/CategoryTheory/Limits/Creates.lean	5	23	['chrisflav', 'erdOne', 'github-actions', 'jcommelin', 'leanprover-community-bot-assistant', 'mathlib-bors']	nobody	28-47382 28 days ago	28-47383 28 days ago	17-3559 17 days
  23528	Ruben-VandeVelde author:Ruben-VandeVelde	feat: add isOpen_setOf_affineIndependent	From sphere-eversion. --- [](https://gitpod.io/from-referrer/)	t-analysis merge-conflict delegated	15/0	Mathlib/Analysis/Normed/Module/FiniteDimension.lean	1	5	['github-actions', 'grunweg', 'leanprover-community-bot-assistant', 'mathlib-bors', 'urkud']	nobody	27-30126 27 days ago	27-30127 27 days ago	26-70139 26 days
  26934	mariainesdff author:mariainesdff	feat(RingTheory/DedekindDomain/Ideal): add HeightOneSpectrum.ofPrime	Previously #24036. Co-authored-by: @Louddy --- [](https://gitpod.io/from-referrer/)	t-ring-theory merge-conflict delegated	9/0	Mathlib/RingTheory/DedekindDomain/Ideal.lean	1	7	['Louddy', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib-bors', 'riccardobrasca']	riccardobrasca assignee:riccardobrasca	11-29514 11 days ago	11-29514 11 days ago	22-14439 22 days

Review status

There are currently 503 PRs awaiting review. Among these,

• 18 are labelled easy (these ones),
• 7 are addressing technical debt (namely these), and
• 212 appeared on the review queue within the last two weeks.

On the other hand, 77 PRs are unassigned and have not seen a status change in a week, and 167 PRs are assigned, without recent review activity.

Stale unassigned PRs on the review queue

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Approval(s)	Updated	Last status change	total time in review
24050	Paul-Lez author:Paul-Lez	feat(Data/Finsupp/Pointwise): generalise pointwise scalar multiplication of finsupps	As pointed out by @eric-wieser, this creates an instance diamond with `SMul (α → β) (α →₀ (α → β))` --- [](https://gitpod.io/from-referrer/)	t-data	7/4	Mathlib/Data/Finsupp/Pointwise.lean	1	6	['Paul-Lez', 'eric-wieser', 'github-actions']	nobody	none	86-29659 2 months ago	128-17957 4 months ago	128-18005 128 days
26284	plp127 author:plp127	feat: faster implementation of `Nat.primeFactorsList` + `@[csimp]` lemma	Add a function `Nat.primeFactorsListFast` that `#eval`s faster, and a `@[csimp]` lemma `Nat.primeFactorsList_eq_primeFactorsListFast` that shows `Nat.primeFactorsList = Nat.primeFactorsListFast`. --- [](https://gitpod.io/from-referrer/)	t-data	95/0	Mathlib/Data/Nat/Factors.lean	1	1	['github-actions']	nobody	none	58-74988 1 month ago	58-75011 1 month ago	59-2526 59 days
26710	metakunt author:metakunt	feat (Data/Nat/Digits/Lemmas): Add digits_getD	Adds digits_getD, an explicit computation of the i-th digits of n in base b representation.	t-data new-contributor	64/0	Mathlib/Data/Nat/Digits/Lemmas.lean	1	1	['github-actions']	nobody	none	48-4682 1 month ago	48-4813 1 month ago	48-4865 48 days
26021	vasnesterov author:vasnesterov	feat(Data/Real): representation of reals from `[0, 1]` in positional system	* Introduce `ofDigits {b : ℕ} (digits : ℕ → Fin b) : ℝ`, representing a real number of the form `0.d₀d₁d₂...` (where `dᵢ = digits i`) as an infinite sum. * Prove that this sum converges to a number in the interval `[0, 1]`. * Prove `ofDigits_close_of_common_prefix`: if the first `n` digits of two numbers are equal, then their difference is bounded by `b⁻ⁿ`. * Introduce `Real.digits`, which converts a real number into its sequence of digits. * Prove that `ofDigits (toDigits x b) = x`. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Base.20n.20expansion.20of.20real.20numbers.3F/near/502937293) --- - [x] depends on: #26004 [](https://gitpod.io/from-referrer/)	t-data	238/0	Mathlib.lean,Mathlib/Data/Real/OfDigits.lean,scripts/noshake.json	3	11	['alreadydone', 'eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'vasnesterov', 'wwylele']	nobody	none	46-63599 1 month ago	49-78367 1 month ago	49-78925 49 days
26838	vlad902 author:vlad902	feat: add lemmas about `List.scanr`	This PR continues the work from #25188. Original PR: https://github.com/leanprover-community/mathlib4/pull/25188	t-data	84/19	Mathlib/Data/List/Scan.lean	1	12	['github-actions', 'vihdzp', 'vlad902']	nobody	none	39-62464 1 month ago	44-64973 1 month ago	44-65027 44 days
27242	hugh-fox author:hugh-fox	feat: add Gauss-like formula for sums of digit sums	Adds `sum_digit_sum_base_pow_eq` to show a Gauss-like formula across sums of digit sums. This relies on an additional two simp lemmas, named `digits_sum_eq_self`, `digits_sum_base_mul_cancel`. Lastly, includes a specialization (which is a good bit simpler than the general formula) to base 10 named `sum_digit_sum_ten_pow_eq`. --- [](https://gitpod.io/from-referrer/)	large-import t-data new-contributor	113/0	Mathlib/Data/Nat/Digits/Lemmas.lean	1	5	['github-actions', 'hugh-fox', 'kckennylau']	nobody	none	32-17978 1 month ago	33-81756 1 month ago	33-81802 33 days
27500	Komyyy author:Komyyy	feat: the Riemann zeta function is meromorphic	Also proves that the Hurwitz zeta function is meromorphic. This PR is split from #27499 to leave a good git diff history. --- The `large-import` change occurs only in the new module, so it poses no problem. - [x] depends on: #27499 This PR continues the work from #25597. Original PR: https://github.com/leanprover-community/mathlib4/pull/25597	large-import t-analysis	51/3	Mathlib.lean,Mathlib/Analysis/Meromorphic/Complex.lean,Mathlib/Analysis/Meromorphic/Gamma.lean	3	2	['github-actions', 'mathlib4-dependent-issues-bot']	nobody	none	24-78922 24 days ago	24-79738 24 days ago	24-80354 24 days
27548	euprunin author:euprunin	chore(Control/Functor/Multivariate): remove use of `erw` in `f` (`private def f`)		t-data	1/1	Mathlib/Control/Functor/Multivariate.lean	1	1	['github-actions']	nobody	none	24-36548 24 days ago	24-36554 24 days ago	24-36606 24 days
27566	wwylele author:wwylele	feat(Data/Real): Archimedean.embedReal is a ring hom when M is an ordered ring	Also shows that this ends up the same as `LinearOrderedField.inducedOrderRingHom` for fields --- This is a spin-off from #27268 ~~because I got bored~~ . This is not in a high priority as I don't need it for anything yet, but the last lemma shows that `embedReal` is a generalization of `LinearOrderedField.inducedOrderRingHom` (which is only stated for field, and I didn't find when I was making the group embedding). Perhaps we should refactor `Mathlib/Algebra/Order/CompleteField.lean` with the definition here. Indeed, if we replace every `ℝ` with `(R : Type*)[ConditionallyCompleteLinearOrderedField R]` in `Data/Real/Embedding.lean`, the proof still works. What do you think? [](https://gitpod.io/from-referrer/)	large-import t-data	220/3	Mathlib/Data/Real/Embedding.lean	1	1	['github-actions']	nobody	none	24-16519 24 days ago	24-16526 24 days ago	24-16579 24 days
27682	FernandoChu author:FernandoChu	Chore: Added `vecAppend_empty` lemma	Added the `vecAppend_empty`.	t-data new-contributor	5/0	Mathlib/Data/Fin/VecNotation.lean	1	1	['github-actions']	nobody	none	21-41186 21 days ago	21-41186 21 days ago	21-41397 21 days
27697	BoltonBailey author:BoltonBailey	chore(Data/Fintype): use `univ` instead of `Fintype.elems`	A short PR to keep the API consistent with its surroundings. --- [](https://gitpod.io/from-referrer/)	t-data	2/2	Mathlib/Data/Fintype/Defs.lean	1	1	['github-actions', 'vihdzp']	nobody	1	21-16779 21 days ago	21-20658 21 days ago	21-20704 21 days
27738	ChrisHughes24 author:ChrisHughes24	feat(Rat): Decidable instance for IsSquare	--- [](https://gitpod.io/from-referrer/)	t-data	3/0	Mathlib/Data/Rat/Lemmas.lean	1	1	['github-actions']	nobody	none	20-57394 20 days ago	20-57398 20 days ago	20-57446 20 days
27742	ChrisHughes24 author:ChrisHughes24	feat(Nat/nth): inequalities about Nat.nth	--- [](https://gitpod.io/from-referrer/)	t-data	58/0	Mathlib/Data/Nat/Nth.lean	1	1	['github-actions']	nobody	none	20-51842 20 days ago	20-51850 20 days ago	20-51896 20 days
27820	FLDutchmann author:FLDutchmann	chore(NumberTheory/SelbergSieve): turn `BoundingSieve` into a struct	Based on a discussion [on zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/BoundingSieve.20is.20a.20class.3F.3F). I wound up removing the custom notation as well, since not everybody was fond of it and I had some trouble getting it to work properly with structure inheritance and the corresponding coersions. --- [](https://gitpod.io/from-referrer/)	t-analysis t-number-theory	51/84	Mathlib/NumberTheory/SelbergSieve.lean	1	1	['github-actions']	nobody	none	19-44655 19 days ago	19-44678 19 days ago	19-44714 19 days
27864	BoltonBailey author:BoltonBailey	feat(Data/{Finset,Multiset}/Sort): give sort functions ≤ default argument	Changes the `Finset.sort` and `Multiset.sort` functions to take `≤` as the default relation argument. Then removes this argument where possible through the rest of the library. This involves switching the order of arguments, but I think this is fine, as this function is mostly called by dot notation anyway, and I think it is more typical for the first argument of such functions to have the type that matches the namespace. Thanks to @eric-wieser for suggesting this approach --- [](https://gitpod.io/from-referrer/)	t-data	121/97	Mathlib/Algebra/Polynomial/Basic.lean,Mathlib/Data/Finset/Sort.lean,Mathlib/Data/Multiset/Sort.lean,Mathlib/Data/Nat/Nth.lean,Mathlib/GroupTheory/Perm/Cycle/Factors.lean,Mathlib/GroupTheory/Perm/Sign.lean,Mathlib/Logic/Equiv/Finset.lean,Mathlib/Logic/Equiv/Multiset.lean,Mathlib/NumberTheory/ADEInequality.lean	9	4	['BoltonBailey', 'eric-wieser', 'github-actions']	nobody	none	18-36160 18 days ago	18-36160 18 days ago	19-3300 19 days
25920	BoltonBailey author:BoltonBailey	feat(Data/Finsupp/Basic): `Finsupp.optionElim'`	Similar to how Finsupp.cons constructs a map Fin (n + 1) →₀ M from a map Fin n →₀ M, we define Finsupp.optionElim' to construct a map Option α →₀ M from a map α →₀ M, given an additional value for none. We base this on the new optionEquiv definition. As a function, it behaves as Option.elim', hence the name. We prove a variety of API lemmas, based on those for Finsupp.cons, to bring the definitions more in line with the contents of Data/Finsupp/Fin. We also refactor to a new file to help avoid a too-long file and make this more analogous to Finsupp.cons Original PR: https://github.com/leanprover-community/mathlib4/pull/13861 - [x] depends on: #26309	migrated-from-branch t-data	124/25	Mathlib/Algebra/Category/MonCat/Adjunctions.lean,Mathlib/Data/Finsupp/Option.lean	2	14	['BoltonBailey', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot']	nobody	none	18-34104 18 days ago	32-80850 1 month ago	55-1433 55 days
26914	quangvdao author:quangvdao	feat(Data/PFunctor/Univariate): more definitions for univariate `PFunctor`	This PR defines several basic definitions of `PFunctor`, including zero, one, constants, monomials, coproduct (sum), product, sigma, pi, tensor product, universe lifting, and equivalence. We also add: (1) simple lemmas connecting the basic definitions, (2) an automatically derived ext lemma for `PFunctor` via `@[ext]` attribute Some things I'm not clear on: - I define `HAdd` and `HMul` instances for coproduct and product of poly functors having different universe levels. Should I also define `Add` and `Mul` instances for poly functors having the same universe level? - Is it ok to define notation for tensor product, i.e. `@[inherit_doc] scoped infixr:80 " ⊗ " => tensor`? I'm worried it might clash with other notation. - Need a double-check on the priority of notation. Some future definitions to add: - Various equivalences arising from arithmetic identities, e.g., `P + 0 ≃ₚ P`. - Definitions of Lenses and Charts (each of them will be a file or even a folder) - Exponential objects (corresponding to both `prod` and `tensor`) --- [](https://gitpod.io/from-referrer/)	t-data	144/5	Mathlib/Data/PFunctor/Univariate/Basic.lean	1	19	['alexkeizer', 'eric-wieser', 'github-actions', 'quangvdao']	nobody	1	17-3997 17 days ago	43-2506 1 month ago	43-2551 43 days
27933	grunweg author:grunweg	chore(OrdNode): format code example in code blocks	Wrap them in code blocks (and unindent them; that indentation is not needed any more). This also avoids warnings from the linter in #27898. ------- [](https://gitpod.io/from-referrer/)	t-data	459/212	Mathlib/Data/Ordmap/Ordnode.lean	1	3	['eric-wieser', 'github-actions', 'grunweg']	nobody	none	16-52020 16 days ago	16-60536 16 days ago	16-60583 16 days
27926	euprunin author:euprunin	chore(Geometry/RingedSpace): remove one porting note and one `erw`	--- Show trace profiling of colimitPresheafObjIsoComponentwiseLimit_inv_ι_app ### Trace profiling of `colimitPresheafObjIsoComponentwiseLimit_inv_ι_app` before PR 27926 ``` info: Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean:318:0: [Elab.command] [1.040188] @[simp] theorem colimitPresheafObjIsoComponentwiseLimit_inv_ι_app (F : J ⥤ PresheafedSpace.{_, _, v} C) (U : Opens (Limits.colimit F).carrier) (j : J) : (colimitPresheafObjIsoComponentwiseLimit F U).inv ≫ (colimit.ι F j).c.app (op U) = limit.π _ (op j) := by delta colimitPresheafObjIsoComponentwiseLimit rw [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)] dsimp rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc] erw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] -- Porting note: `convert` doesn't work due to meta variable, so change to a `suffices` block set f := _ change _ ≫ f = _ suffices f_eq : f = 𝟙 _ by rw [f_eq, comp_id] erw [← (F.obj j).presheaf.map_id] change (F.obj j).presheaf.map _ ≫ _ = _ simp [Elab.definition.header] [0.097144] AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app [Elab.step] [0.025268] expected type: Type v, term Opens (Limits.colimit F).carrier [Elab.step] [0.020151] expected type: Type ?u.174516, term (Limits.colimit F).carrier [Elab.step] [0.019933] expected type: , term (Limits.colimit F) [Elab.step] [0.019920] expected type: , term Limits.colimit F [Meta.synthInstance] [0.018758] ✅️ HasColimit F [Elab.step] [0.070061] expected type: Prop, term (colimitPresheafObjIsoComponentwiseLimit F U).inv ≫ (colimit.ι F j).c.app (op U) = limit.π _ (op j) [Elab.step] [0.070046] expected type: Prop, term binrel% Eq✝ ((colimitPresheafObjIsoComponentwiseLimit F U).inv ≫ (colimit.ι F j).c.app (op U)) (limit.π _ (op j)) [Meta.synthInstance] [0.058249] ✅️ HasLimit (componentwiseDiagram F U) [Elab.attribute] [0.937317] applying [simp] info: Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean:318:0: [Elab.async] [0.937262] elaborating proof of AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app [Elab.definition.value] [0.927035] AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app [Elab.step] [0.922546] delta colimitPresheafObjIsoComponentwiseLimit rw [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)] dsimp rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc] erw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] -- Porting note: `convert` doesn't work due to meta variable, so change to a `suffices` block set f := _ change _ ≫ f = _ suffices f_eq : f = 𝟙 _ by rw [f_eq, comp_id] erw [← (F.obj j).presheaf.map_id] change (F.obj j).presheaf.map _ ≫ _ = _ simp [Elab.step] [0.922530] delta colimitPresheafObjIsoComponentwiseLimit rw [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)] dsimp rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc] erw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] -- Porting note: `convert` doesn't work due to meta variable, so change to a `suffices` block set f := _ change _ ≫ f = _ suffices f_eq : f = 𝟙 _ by rw [f_eq, comp_id] erw [← (F.obj j).presheaf.map_id] change (F.obj j).presheaf.map _ ≫ _ = _ simp [Elab.step] [0.146177] rw [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)] [Elab.step] [0.146159] (rewrite [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)]; with_annotate_state"]" (try (with_reducible rfl))) [Elab.step] [0.146150] rewrite [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.146140] rewrite [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.144815] rewrite [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)] [Meta.check] [0.016973] ✅️ fun _a ↦ (((Limits.lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).inv) ≫ _a) ≫ (colimit.ι F j).c.app (op U) = limit.π (componentwiseDiagram F U) (op j) [Meta.check] [0.014416] ✅️ fun _a ↦ (((Limits.lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).inv) ≫ _a.app (op U)) ≫ (colimit.ι F j).c.app (op U) = limit.π (componentwiseDiagram F U) (op j) [Meta.check] [0.010654] ✅️ fun _a ↦ (((Limits.lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).inv) ≫ _a) ≫ (colimit.ι F j).c.app (op U) = limit.π (componentwiseDiagram F U) (op j) [Meta.check] [0.023805] ✅️ fun _a ↦ (((Limits.lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).inv) ≫ _a ≫ (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫ (colimit.ι F j).c.app (op U) = limit.π (componentwiseDiagram F U) (op j) [Elab.step] [0.046171] dsimp [Elab.step] [0.362200] rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc] [Elab.step] [0.361801] (rewrite [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc]; with_annotate_state"]" (try (with_reducible rfl))) [Elab.step] [0.361793] rewrite [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.361787] rewrite [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.361130] rewrite [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc] [Meta.check] [0.046061] ✅️ fun _a ↦ ((limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv) ≫ ((colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ _a) ≫ (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫ (colimit.ι F j).c.app (op U) = limit.π (componentwiseDiagram F U) (op j) [Meta.isDefEq] [0.014339] ✅️ autoParam (∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f) _auto✝ =?= ∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f [Meta.isDefEq] [0.014330] ✅️ ∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f =?= ∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f [Meta.isDefEq] [0.014288] ✅️ ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f =?= ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f [Meta.isDefEq] [0.013035] ✅️ ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom =?= ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom [Meta.isDefEq] [0.013017] ✅️ inst✝³.toCategoryStruct.3 (((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f) (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom =?= inst✝³.toCategoryStruct.3 (((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f) (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom [Meta.check] [0.027427] ✅️ fun _a ↦ ((limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv) ≫ _a ≫ (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫ (colimit.ι F j).c.app (op U) = limit.π (componentwiseDiagram F U) (op j) [Meta.check] [0.019082] ✅️ fun _a ↦ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ _a = limit.π (componentwiseDiagram F U) (op j) [Meta.check] [0.023213] ✅️ fun _a ↦ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ _a = limit.π (componentwiseDiagram F U) (op j) [Meta.isDefEq] [0.014000] ✅️ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ (colimit.ι F j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =?= (Hom.c ?β).app ?U ≫ (Hom.c ?α).app (op ((Opens.map (Hom.base ?β)).obj (unop ?U))) ≫ ?h [Meta.isDefEq] [0.011423] ✅️ (colimit.ι F j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =?= (Hom.c ?α).app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj (unop (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))))) ≫ ?h [Meta.check] [0.019734] ✅️ fun _a ↦ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ _a = limit.π (componentwiseDiagram F U) (op j) [Meta.check] [0.041226] ✅️ fun _a ↦ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ _a ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) = limit.π (componentwiseDiagram F U) (op j) [Meta.isDefEq] [0.013545] ✅️ (({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ (F.obj j).presheaf.map (eqToHom ⋯)) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =?= (?f ≫ ?g) ≫ ?h [Meta.check] [0.022526] ✅️ fun _a ↦ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ _a = limit.π (componentwiseDiagram F U) (op j) [Meta.isDefEq] [0.010494] ✅️ autoParam (∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f) _auto✝ =?= ∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f [Meta.isDefEq] [0.010484] ✅️ ∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f =?= ∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f [Meta.isDefEq] [0.010433] ✅️ ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f =?= ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f [Elab.step] [0.153503] erw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] [Elab.step] [0.149349] rw (transparency✝ := .default✝) [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] [Elab.step] [0.149342] (rewrite (transparency✝ := .default✝) [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc]; with_annotate_state"]" (try (with_reducible rfl))) [Elab.step] [0.149338] rewrite (transparency✝ := .default✝) [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.149333] rewrite (transparency✝ := .default✝) [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.148668] rewrite (transparency✝ := .default✝) [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] [Meta.isDefEq] [0.018626] ✅️ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ (F.obj j).presheaf.map (eqToHom ⋯) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =?= (limitObjIsoLimitCompEvaluation ?F ?k).inv ≫ (limit.π ?F ?j).app ?k ≫ ?h [Meta.isDefEq.delta] [0.018438] ✅️ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ (F.obj j).presheaf.map (eqToHom ⋯) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =?= (limitObjIsoLimitCompEvaluation ?F ?k).inv ≫ (limit.π ?F ?j).app ?k ≫ ?h [Meta.isDefEq] [0.015684] ✅️ ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ (F.obj j).presheaf.map (eqToHom ⋯) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =?= (limit.π (pushforwardDiagramToColimit F).leftOp ?j).app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ ?h [Meta.isDefEq.delta] [0.015635] ✅️ ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ (F.obj j).presheaf.map (eqToHom ⋯) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =?= (limit.π (pushforwardDiagramToColimit F).leftOp ?j).app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ ?h [Meta.isDefEq] [0.012504] ✅️ ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) =?= (limit.π (pushforwardDiagramToColimit F).leftOp ?j).app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) [Meta.isDefEq.delta] [0.012467] ✅️ ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) =?= (limit.π (pushforwardDiagramToColimit F).leftOp ?j).app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) [Meta.check] [0.032205] ✅️ fun _a ↦ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ _a = limit.π (componentwiseDiagram F U) (op j) [Meta.isDefEq] [0.011807] ✅️ autoParam (∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f) _auto✝ =?= ∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f [Meta.isDefEq] [0.011776] ✅️ ∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f =?= ∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f [Meta.isDefEq] [0.011697] ✅️ ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f =?= ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f [Meta.isDefEq] [0.010926] ✅️ ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom =?= ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom [Meta.isDefEq] [0.010889] ✅️ inst✝³.toCategoryStruct.3 (((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f) (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom =?= inst✝³.toCategoryStruct.3 (((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f) (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom [Meta.synthInstance] [0.032731] ✅️ HasLimit (componentwiseDiagram F U) [Meta.synthInstance] [0.037409] ✅️ HasLimit ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Elab.step] [0.014221] suffices f_eq : f = 𝟙 _ by rw [f_eq, comp_id] [Elab.step] [0.012150] refine_lift suffices f_eq : f = 𝟙 _ by rw [f_eq, comp_id]; ?_ [Elab.step] [0.012144] focus (refine no_implicit_lambda% (suffices f_eq : f = 𝟙 _ by rw [f_eq, comp_id]; ?_); rotate_right) [Elab.step] [0.012137] (refine no_implicit_lambda% (suffices f_eq : f = 𝟙 _ by rw [f_eq, comp_id]; ?_); rotate_right) [Elab.step] [0.012133] (refine no_implicit_lambda% (suffices f_eq : f = 𝟙 _ by rw [f_eq, comp_id]; ?_); rotate_right) [Elab.step] [0.012129] (refine no_implicit_lambda% (suffices f_eq : f = 𝟙 _ by rw [f_eq, comp_id]; ?_); rotate_right) [Elab.step] [0.012125] refine no_implicit_lambda% (suffices f_eq : f = 𝟙 _ by rw [f_eq, comp_id]; ?_); rotate_right [Elab.step] [0.012121] refine no_implicit_lambda% (suffices f_eq : f = 𝟙 _ by rw [f_eq, comp_id]; ?_); rotate_right [Elab.step] [0.012108] refine no_implicit_lambda% (suffices f_eq : f = 𝟙 _ by rw [f_eq, comp_id]; ?_) [Elab.step] [0.013093] change (F.obj j).presheaf.map _ ≫ _ = _ [Elab.step] [0.168494] simp [Meta.isDefEq] [0.021985] ❌️ eqToHom ?p =?= eqToHom ⋯ [Meta.isDefEq] [0.021872] ❌️ ?p =?= colimit.isoColimitCocone_ι_hom { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F } j ▸ Eq.refl ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq] [0.021293] ❌️ eqToHom ?p =?= eqToHom ⋯ [Meta.isDefEq] [0.021164] ❌️ ?p =?= colimit.isoColimitCocone_ι_hom { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F } j ▸ Eq.refl ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq] [0.010555] ✅️ (toPrefunctor ?F).map (eqToHom ?p) =?= (F.obj j).presheaf.map (eqToHom ⋯) [Meta.isDefEq.delta] [0.010532] ✅️ (toPrefunctor ?F).map (eqToHom ?p) =?= (F.obj j).presheaf.map (eqToHom ⋯) [Meta.isDefEq] [0.010242] ✅️ eqToHom ?p =?= eqToHom ⋯ [Meta.isDefEq] [0.010214] ✅️ ?p =?= colimit.isoColimitCocone_ι_hom { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F } j ▸ Eq.refl ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq.assign] [0.010212] ✅️ ?p := colimit.isoColimitCocone_ι_hom { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F } j ▸ Eq.refl ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq.assign.checkTypes] [0.010174] ✅️ (?p : op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = op ((Opens.map (colimit.ι F j).base).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)))) := (colimit.isoColimitCocone_ι_hom { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F } j ▸ Eq.refl ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) : (Opens.map ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq] [0.010170] ✅️ op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = op ((Opens.map (colimit.ι F j).base).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) =?= (Opens.map ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) info: Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean:319:8: [Elab.async] [0.072478] Lean.addDecl [Kernel] [0.072444] typechecking declarations [AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app] ``` ### Trace profiling of `colimitPresheafObjIsoComponentwiseLimit_inv_ι_app` after PR 27926 ```diff diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean index 5771499b70..cbf879186d 100644 --- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean +++ b/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean @@ -316,2 +316,3 @@ def colimitPresheafObjIsoComponentwiseLimit (F : J ⥤ PresheafedSpace.{_, _, v} +set_option trace.profiler true in @[simp] @@ -329,8 +330,2 @@ theorem colimitPresheafObjIsoComponentwiseLimit_inv_ι_app (F : J ⥤ Presheafed erw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] - -- Porting note: `convert` doesn't work due to meta variable, so change to a `suffices` block - set f := _ - change _ ≫ f = _ - suffices f_eq : f = 𝟙 _ by rw [f_eq, comp_id] - erw [← (F.obj j).presheaf.map_id] - change (F.obj j).presheaf.map _ ≫ _ = _ simp ``` ``` info: Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean:318:0: [Elab.command] [1.024539] @[simp] theorem colimitPresheafObjIsoComponentwiseLimit_inv_ι_app (F : J ⥤ PresheafedSpace.{_, _, v} C) (U : Opens (Limits.colimit F).carrier) (j : J) : (colimitPresheafObjIsoComponentwiseLimit F U).inv ≫ (colimit.ι F j).c.app (op U) = limit.π _ (op j) := by delta colimitPresheafObjIsoComponentwiseLimit rw [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)] dsimp rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc] erw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] simp [Elab.definition.header] [0.078196] AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app [Elab.step] [0.012578] expected type: Type v, term Opens (Limits.colimit F).carrier [Elab.step] [0.064806] expected type: Prop, term (colimitPresheafObjIsoComponentwiseLimit F U).inv ≫ (colimit.ι F j).c.app (op U) = limit.π _ (op j) [Elab.step] [0.064794] expected type: Prop, term binrel% Eq✝ ((colimitPresheafObjIsoComponentwiseLimit F U).inv ≫ (colimit.ι F j).c.app (op U)) (limit.π _ (op j)) [Meta.synthInstance] [0.046124] ✅️ HasLimit (componentwiseDiagram F U) [Elab.attribute] [0.941447] applying [simp] info: Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean:318:0: [Elab.async] [0.941493] elaborating proof of AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app [Elab.definition.value] [0.933934] AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app [Elab.step] [0.922601] delta colimitPresheafObjIsoComponentwiseLimit rw [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)] dsimp rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc] erw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] simp [Elab.step] [0.922582] delta colimitPresheafObjIsoComponentwiseLimit rw [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)] dsimp rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc] erw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] simp [Elab.step] [0.135785] rw [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)] [Elab.step] [0.135770] (rewrite [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)]; with_annotate_state"]" (try (with_reducible rfl))) [Elab.step] [0.135762] rewrite [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.135756] rewrite [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.135146] rewrite [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app, congr_app (Iso.symm_inv _)] [Meta.check] [0.011988] ✅️ fun _a ↦ (((Limits.lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).inv) ≫ _a) ≫ (colimit.ι F j).c.app (op U) = limit.π (componentwiseDiagram F U) (op j) [Meta.check] [0.013908] ✅️ fun _a ↦ (((Limits.lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).inv) ≫ _a.app (op U)) ≫ (colimit.ι F j).c.app (op U) = limit.π (componentwiseDiagram F U) (op j) [Meta.check] [0.010543] ✅️ fun _a ↦ (((Limits.lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).inv) ≫ _a) ≫ (colimit.ι F j).c.app (op U) = limit.π (componentwiseDiagram F U) (op j) [Meta.check] [0.020840] ✅️ fun _a ↦ (((Limits.lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).inv) ≫ _a ≫ (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫ (colimit.ι F j).c.app (op U) = limit.π (componentwiseDiagram F U) (op j) [Elab.step] [0.043416] dsimp [Elab.step] [0.347288] rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc] [Elab.step] [0.347048] (rewrite [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc]; with_annotate_state"]" (try (with_reducible rfl))) [Elab.step] [0.347040] rewrite [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.347035] rewrite [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.346402] rewrite [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc] [Meta.check] [0.032750] ✅️ fun _a ↦ ((limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv) ≫ ((colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ _a) ≫ (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫ (colimit.ι F j).c.app (op U) = limit.π (componentwiseDiagram F U) (op j) [Meta.check] [0.028063] ✅️ fun _a ↦ ((limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv) ≫ _a ≫ (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫ (colimit.ι F j).c.app (op U) = limit.π (componentwiseDiagram F U) (op j) [Meta.check] [0.019057] ✅️ fun _a ↦ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ _a = limit.π (componentwiseDiagram F U) (op j) [Meta.check] [0.022883] ✅️ fun _a ↦ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ _a = limit.π (componentwiseDiagram F U) (op j) [Meta.isDefEq] [0.013327] ✅️ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ (colimit.ι F j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =?= (Hom.c ?β).app ?U ≫ (Hom.c ?α).app (op ((Opens.map (Hom.base ?β)).obj (unop ?U))) ≫ ?h [Meta.isDefEq] [0.011046] ✅️ (colimit.ι F j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =?= (Hom.c ?α).app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj (unop (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))))) ≫ ?h [Meta.check] [0.019487] ✅️ fun _a ↦ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ _a = limit.π (componentwiseDiagram F U) (op j) [Meta.check] [0.042766] ✅️ fun _a ↦ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ _a ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) = limit.π (componentwiseDiagram F U) (op j) [Meta.isDefEq] [0.013346] ✅️ (({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ (F.obj j).presheaf.map (eqToHom ⋯)) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =?= (?f ≫ ?g) ≫ ?h [Meta.check] [0.019948] ✅️ fun _a ↦ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ _a = limit.π (componentwiseDiagram F U) (op j) [Elab.step] [0.157932] erw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] [Elab.step] [0.154595] rw (transparency✝ := .default✝) [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] [Elab.step] [0.154588] (rewrite (transparency✝ := .default✝) [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc]; with_annotate_state"]" (try (with_reducible rfl))) [Elab.step] [0.154584] rewrite (transparency✝ := .default✝) [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.154579] rewrite (transparency✝ := .default✝) [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc]; with_annotate_state"]" (try (with_reducible rfl)) [Elab.step] [0.153927] rewrite (transparency✝ := .default✝) [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] [Meta.isDefEq] [0.012088] ✅️ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ (F.obj j).presheaf.map (eqToHom ⋯) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =?= (limitObjIsoLimitCompEvaluation ?F ?k).inv ≫ (limit.π ?F ?j).app ?k ≫ ?h [Meta.isDefEq.delta] [0.012000] ✅️ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).inv ≫ ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).c.app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ (F.obj j).presheaf.map (eqToHom ⋯) ≫ ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =?= (limitObjIsoLimitCompEvaluation ?F ?k).inv ≫ (limit.π ?F ?j).app ?k ≫ ?h [Meta.check] [0.023999] ✅️ fun _a ↦ limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫ _a = limit.π (componentwiseDiagram F U) (op j) [Meta.synthInstance] [0.043793] ✅️ HasLimit (componentwiseDiagram F U) [Meta.synthInstance] [0.050911] ✅️ HasLimit ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Elab.step] [0.237283] simp [Meta.isDefEq] [0.020018] ✅️ (NatIso.ofComponents ?app ?naturality).inv.app ?X =?= (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv.app (op j) [Meta.isDefEq.delta] [0.019991] ✅️ (NatIso.ofComponents ?app ?naturality).inv.app ?X =?= (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv.app (op j) [Meta.isDefEq] [0.019797] ✅️ (NatIso.ofComponents ?app ?naturality).inv =?= (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv [Meta.isDefEq.delta] [0.019779] ✅️ (NatIso.ofComponents ?app ?naturality).inv =?= (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv [Meta.isDefEq] [0.019743] ✅️ NatIso.ofComponents ?app ?naturality =?= NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯ [Meta.isDefEq] [0.017808] ✅️ ?naturality =?= @colimitPresheafObjIsoComponentwiseLimit._proof_5 J inst✝⁴ C inst✝³ inst✝² inst✝¹ inst✝ F (hasColimitOfHasColimitsOfShape F) U [Meta.isDefEq.assign] [0.017806] ✅️ ?naturality := @colimitPresheafObjIsoComponentwiseLimit._proof_5 J inst✝⁴ C inst✝³ inst✝² inst✝¹ inst✝ F (hasColimitOfHasColimitsOfShape F) U [Meta.isDefEq.assign.checkTypes] [0.017713] ✅️ (?naturality : autoParam (∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f) _auto✝) := (@colimitPresheafObjIsoComponentwiseLimit._proof_5 J inst✝⁴ C inst✝³ inst✝² inst✝¹ inst✝ F (hasColimitOfHasColimitsOfShape F) U : ∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f) [Meta.isDefEq] [0.017709] ✅️ autoParam (∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f) _auto✝ =?= ∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f [Meta.isDefEq] [0.017679] ✅️ ∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f =?= ∀ {X Y : Jᵒᵖ} (f : X ⟶ Y), ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f [Meta.isDefEq] [0.017646] ✅️ ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f =?= ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom = (mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)).hom ≫ (componentwiseDiagram F U).map f [Meta.isDefEq] [0.016839] ✅️ ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom =?= ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f ≫ (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom [Meta.isDefEq] [0.016824] ✅️ inst✝³.toCategoryStruct.3 (((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f) (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom =?= inst✝³.toCategoryStruct.3 (((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f) (mapIso (F.obj (unop Y)).presheaf (eqToIso ⋯)).hom [Meta.isDefEq] [0.014645] ✅️ ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map f =?= ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map f [Meta.isDefEq] [0.014628] ✅️ ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).toPrefunctor.2 f =?= ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).toPrefunctor.2 f [Meta.isDefEq] [0.014549] ✅️ ((evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).map ((pushforwardDiagramToColimit F).leftOp.map f) =?= ((evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).map ((pushforwardDiagramToColimit F).leftOp.map f) [Meta.isDefEq] [0.014534] ✅️ ((evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))).toPrefunctor.2 ((pushforwardDiagramToColimit F).leftOp.map f) =?= ((evaluation (Opens ↑↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt)ᵒᵖ C).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))).toPrefunctor.2 ((pushforwardDiagramToColimit F).leftOp.map f) [Meta.isDefEq] [0.014406] ✅️ ((pushforwardDiagramToColimit F).leftOp.map f).app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) =?= ((pushforwardDiagramToColimit F).leftOp.map f).app ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U)) [Meta.isDefEq] [0.014386] ✅️ ((pushforwardDiagramToColimit F).leftOp.map f).1 (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) =?= ((pushforwardDiagramToColimit F).leftOp.map f).1 ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U)) [Meta.isDefEq] [0.010919] ✅️ ((pushforward C (colimit.ι (F ⋙ forget C) (unop X))).map (F.map f.unop).c).app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) ≫ ((Pushforward.comp ((F ⋙ forget C).map f.unop) (colimit.ι (F ⋙ forget C) (unop X)) (F.obj (unop Y)).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj (unop Y)).presheaf).hom).app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) =?= ((pushforward C (colimit.ι (F ⋙ forget C) (unop X))).map (F.map f.unop).c).app ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U)) ≫ ((Pushforward.comp ((F ⋙ forget C).map f.unop) (colimit.ι (F ⋙ forget C) (unop X)) (F.obj (unop Y)).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj (unop Y)).presheaf).hom).app ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U)) [Meta.isDefEq] [0.010872] ✅️ inst✝³.toCategoryStruct.3 (((pushforward C (colimit.ι (F ⋙ forget C) (unop X))).map (F.map f.unop).c).app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) (((Pushforward.comp ((F ⋙ forget C).map f.unop) (colimit.ι (F ⋙ forget C) (unop X)) (F.obj (unop Y)).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj (unop Y)).presheaf).hom).app (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) =?= inst✝³.toCategoryStruct.3 (((pushforward C (colimit.ι (F ⋙ forget C) (unop X))).map (F.map f.unop).c).app ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))) (((Pushforward.comp ((F ⋙ forget C).map f.unop) (colimit.ι (F ⋙ forget C) (unop X)) (F.obj (unop Y)).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj (unop Y)).presheaf).hom).app ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj (op U))) [Meta.isDefEq] [0.036880] ❌️ eqToHom ?p =?= eqToHom ⋯ [Meta.isDefEq] [0.036754] ❌️ ?p =?= colimit.isoColimitCocone_ι_hom { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F } j ▸ Eq.refl ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq.assign] [0.014492] ❌️ ?p := colimit.isoColimitCocone_ι_hom { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F } j ▸ Eq.refl ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq.assign.checkTypes] [0.014435] ❌️ (?p : op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) := (colimit.isoColimitCocone_ι_hom { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F } j ▸ Eq.refl ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) : (Opens.map ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq] [0.014433] ❌️ op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) =?= (Opens.map ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) [Meta.isDefEq] [0.013670] ❌️ op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) =?= (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) [Meta.isDefEq] [0.013662] ❌️ op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) =?= (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.toPrefunctor.1 (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) [Meta.isDefEq] [0.013635] ❌️ op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) =?= op ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).obj (unop (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)))) [Meta.isDefEq] [0.013607] ❌️ (Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U) =?= (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).obj (unop (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq] [0.013597] ❌️ (Opens.map (colimit.ι (F ⋙ forget C) j)).toPrefunctor.1 ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U) =?= (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).toPrefunctor.1 (unop (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq] [0.013549] ❌️ { carrier := ⇑(ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j)) ⁻¹' ↑((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U), is_open' := ⋯ } =?= { carrier := ⇑(ConcreteCategory.hom (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base) ⁻¹' ↑(unop (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))), is_open' := ⋯ } [Meta.isDefEq] [0.013528] ❌️ ⇑(ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j)) ⁻¹' ↑((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U) =?= ⇑(ConcreteCategory.hom (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base) ⁻¹' ↑(unop (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq.delta] [0.010260] ❌️ ⇑(ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j)) ⁻¹' ↑((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U) =?= ⇑(ConcreteCategory.hom (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base) ⁻¹' ↑(unop (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq] [0.010255] ❌️ ⇑(ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j)) =?= ⇑(ConcreteCategory.hom (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base) [Meta.isDefEq] [0.010244] ❌️ ((fun X Y ↦ ContinuousMap.instFunLike) (↑(F.obj j)) (Limits.colimit (F ⋙ forget C))).1 (ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j)) =?= ((fun X Y ↦ ContinuousMap.instFunLike) ↑(F.obj j) ↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt).1 (ConcreteCategory.hom (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base) [Meta.isDefEq] [0.010227] ❌️ (ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j)).toFun =?= (ConcreteCategory.hom (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).toFun [Meta.isDefEq] [0.010215] ❌️ (ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j)).1 =?= (ConcreteCategory.hom (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).1 [Meta.isDefEq.assign] [0.017826] ❌️ ?p := colimit.isoColimitCocone_ι_hom { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F } j ▸ Eq.refl ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq.assign.checkTypes] [0.017754] ❌️ (?p : op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) := (colimit.isoColimitCocone_ι_hom { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F } j ▸ Eq.refl ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) : fun {β} ↦ (Opens.map β.base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq] [0.017751] ❌️ op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) =?= fun {β} ↦ (Opens.map β.base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) [Meta.isDefEq] [0.017746] ❌️ op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) =?= (Opens.map ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) [Meta.isDefEq] [0.017009] ❌️ op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) =?= (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) [Meta.isDefEq] [0.017001] ❌️ op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) =?= (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.toPrefunctor.1 (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) [Meta.isDefEq] [0.016976] ❌️ op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) =?= op ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).obj (unop (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)))) [Meta.isDefEq] [0.016946] ❌️ (Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U) =?= (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).obj (unop (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq] [0.016936] ❌️ (Opens.map (colimit.ι (F ⋙ forget C) j)).toPrefunctor.1 ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U) =?= (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).toPrefunctor.1 (unop (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq] [0.016889] ❌️ { carrier := ⇑(ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j)) ⁻¹' ↑((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U), is_open' := ⋯ } =?= { carrier := ⇑(ConcreteCategory.hom (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base) ⁻¹' ↑(unop (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))), is_open' := ⋯ } [Meta.isDefEq] [0.016868] ❌️ ⇑(ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j)) ⁻¹' ↑((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U) =?= ⇑(ConcreteCategory.hom (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base) ⁻¹' ↑(unop (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq.delta] [0.013665] ❌️ ⇑(ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j)) ⁻¹' ↑((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U) =?= ⇑(ConcreteCategory.hom (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base) ⁻¹' ↑(unop (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq] [0.013661] ❌️ ⇑(ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j)) =?= ⇑(ConcreteCategory.hom (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base) [Meta.isDefEq] [0.013651] ❌️ ((fun X Y ↦ ContinuousMap.instFunLike) (↑(F.obj j)) (Limits.colimit (F ⋙ forget C))).1 (ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j)) =?= ((fun X Y ↦ ContinuousMap.instFunLike) ↑(F.obj j) ↑{ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.pt).1 (ConcreteCategory.hom (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base) [Meta.isDefEq] [0.013633] ❌️ (ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j)).toFun =?= (ConcreteCategory.hom (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).toFun [Meta.isDefEq] [0.013622] ❌️ (ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j)).1 =?= (ConcreteCategory.hom (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).1 [Meta.isDefEq] [0.021315] ❌️ eqToHom ?p =?= eqToHom ⋯ [Meta.isDefEq] [0.021164] ❌️ ?p =?= colimit.isoColimitCocone_ι_hom { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F } j ▸ Eq.refl ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq] [0.010396] ✅️ (toPrefunctor ?F).map (eqToHom ?p) =?= (F.obj j).presheaf.map (eqToHom ⋯) [Meta.isDefEq.delta] [0.010372] ✅️ (toPrefunctor ?F).map (eqToHom ?p) =?= (F.obj j).presheaf.map (eqToHom ⋯) [Meta.isDefEq] [0.010074] ✅️ eqToHom ?p =?= eqToHom ⋯ [Meta.isDefEq] [0.010047] ✅️ ?p =?= colimit.isoColimitCocone_ι_hom { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F } j ▸ Eq.refl ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq.assign] [0.010045] ✅️ ?p := colimit.isoColimitCocone_ι_hom { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F } j ▸ Eq.refl ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq.assign.checkTypes] [0.010004] ✅️ (?p : op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = op ((Opens.map (colimit.ι F j).base).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)))) := (colimit.isoColimitCocone_ι_hom { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F } j ▸ Eq.refl ((Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) : (Opens.map ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) [Meta.isDefEq] [0.010000] ✅️ op ((Opens.map (colimit.ι (F ⋙ forget C) j)).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = op ((Opens.map (colimit.ι F j).base).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U))) =?= (Opens.map ({ cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }.cocone.ι.app j).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) = (Opens.map (colimit.ι F j ≫ (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom).base).op.obj (op ((Opens.map (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj U)) info: Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean:319:8: [Elab.async] [0.056169] Lean.addDecl [Kernel] [0.056142] typechecking declarations [AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app] ```	t-algebraic-geometry	0/6	Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean	1	2	['euprunin', 'github-actions']	nobody	none	16-48676 16 days ago	16-69590 16 days ago	16-69636 16 days
27944	grunweg author:grunweg	feat: lint module names with a period	This would have caught the mis-placed file in #27796. --- [](https://gitpod.io/from-referrer/)	t-linter	16/0	Mathlib/Tactic/Linter/TextBased.lean,scripts/lint-style.lean	2	2	['github-actions', 'grunweg']	nobody	none	16-26819 16 days ago	16-26889 16 days ago	16-26873 16 days
26644	kckennylau author:kckennylau	feat(SetTheory/ZFC): Define the language of sets and state the ZFC axioms	--- [](https://gitpod.io/from-referrer/)	t-set-theory	381/0	Mathlib.lean,Mathlib/SetTheory/ZFC/Axioms.lean,docs/references.bib	3	46	['github-actions', 'kckennylau', 'leanprover-community-bot-assistant', 'staroperator', 'vihdzp']	nobody	none	15-52554 15 days ago	15-52574 15 days ago	36-81913 36 days
27995	kckennylau author:kckennylau	feat(RingTheory/Valuation): alternate constructors for Valuation	--- [](https://gitpod.io/from-referrer/)		69/0	Mathlib/FieldTheory/RatFunc/Degree.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/RingTheory/Valuation/Basic.lean	3	18	['YaelDillies', 'github-actions', 'kckennylau', 'pechersky']	nobody	none	15-17148 15 days ago	15-23312 15 days ago	15-23295 15 days
27392	Paul-Lez author:Paul-Lez	feat(Tactic/SimpUtils): add simproc finding commands	This PR adds some commands to allow users to find simprocs/dsimprocs/simp theorems that match on a given pattern. Thanks to Robin Arnez for telling me about `simprocDeclExt` :) --- [](https://gitpod.io/from-referrer/)	t-meta	690/0	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/SimpUtils.lean,MathlibTest/SimpUtils.lean	4	8	['Paul-Lez', 'eric-wieser', 'github-actions']	nobody	none	15-15379 15 days ago	15-15474 15 days ago	17-16144 17 days
28025	kim-em author:kim-em	feat: grind annotations in Logic/Equiv/Defs		t-logic	153/80	Mathlib/Logic/Equiv/Array.lean,Mathlib/Logic/Equiv/Defs.lean,Mathlib/Logic/Equiv/Embedding.lean,Mathlib/Logic/Equiv/Finset.lean,Mathlib/Logic/Equiv/Fintype.lean,Mathlib/Logic/Equiv/Option.lean,Mathlib/Logic/Equiv/Prod.lean	7	6	['github-actions', 'kim-em', 'leanprover-bot', 'leanprover-community-mathlib4-bot']	nobody	none	14-57883 14 days ago	14-69656 14 days ago	14-75021 14 days
27991	sinianluoye author:sinianluoye	feat (Rat): add Rat.den_eq_of_add_den_eq_one and its dependent lemmas	```lean4 example {q r : ℚ} (h : (q + r).den = 1) : q.den = r.den := by ``` It is so simple, but I couldn't find it in current mathlib repo. --- [](https://gitpod.io/from-referrer/)	t-data new-contributor	28/0	Mathlib/Data/Rat/Lemmas.lean	1	14	['github-actions', 'sinianluoye', 'themathqueen']	nobody	none	13-28014 13 days ago	15-1017 15 days ago	15-29071 15 days
28111	euprunin author:euprunin	chore: remove tactic `simp_lex` and use `simp` instead	Motivation: `simp_lex` is just shorthand for `refine toLex.surjective.forall₃.2 ?_; rintro (a | a) (b | b) (c | c) <;> simp`, so plain `simp` seems preferable.	t-data	4/10	Mathlib/Data/Sum/Interval.lean	1	5	['eric-wieser', 'euprunin', 'github-actions']	nobody	none	12-39087 12 days ago	12-39170 12 days ago	12-46801 12 days
28140	YaelDillies author:YaelDillies	feat: a `PointedCone`-valued version of `Submodule.span`	This is merely to guide typing. From Toric --- [](https://gitpod.io/from-referrer/)	t-convex-geometry toric	10/1	Mathlib/Geometry/Convex/Cone/Pointed.lean	1	1	['github-actions']	nobody	none	11-65185 11 days ago	11-65185 11 days ago	11-65333 11 days
28115	bwangpj author:bwangpj	feat(AlgebraicGeometry/EllipticCurve): reduction of elliptic curves	Define the reduction of elliptic curves over the fraction field of a DVR, following Silverman. --- [](https://gitpod.io/from-referrer/)	new-contributor t-algebraic-geometry	230/1	Mathlib.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Reduction.lean,Mathlib/RingTheory/Valuation/Discrete/Basic.lean	3	14	['Multramate', 'bwangpj', 'github-actions', 'kbuzzard']	nobody	none	10-74384 10 days ago	12-65030 12 days ago	12-65075 12 days
28164	bryangingechen author:bryangingechen	fix(Cache): add put* commands to leanTarArgs	Without this, running `lake exe cache put` fails if `leantar` is not already installed. --- What label should this get? `CI` and `t-meta` don't seem right. [](https://gitpod.io/from-referrer/)	easy	2/2	Cache/Main.lean	1	1	['github-actions']	nobody	none	10-51124 10 days ago	11-14150 11 days ago	11-14134 11 days
28195	gasparattila author:gasparattila	feat: separating a convex compact set and its neighborhood with a polytope	--- [](https://gitpod.io/from-referrer/)	new-contributor t-analysis	26/1	Mathlib/Analysis/Normed/Affine/Convex.lean	1	2	['FrankieNC', 'github-actions']	nobody	none	10-13299 10 days ago	10-17356 10 days ago	10-17410 10 days
28119	JasperMS author:JasperMS	feat(Data/Set/Pairwise): prove pairwise results for Chains, move `Set.pairwise_iUnion₂`	Initiate a new file `Data/Set/Pairwise/Chain.lean` which makes some `Pairwise` results available to the `IsChain` predicate. In the process, move `Set.pairwise_iUnion₂` to group it with similar results. Perform some variable harmonization. Part of Carleson, original result by Edward van de Meent. Moves: - Set.pairwise_iUnion₂: from Data.Set.Lattice to Data.Set.Pairwise.Lattice --- This PR was discussed and advice was given in [#mathlib4 > Novice questions on style and structure](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Novice.20questions.20on.20style.20and.20structure/with/533462814). Many thanks to those who helped me out! Mathlib PRs are still new to me, so please point out where I can improve! [](https://gitpod.io/from-referrer/)	carleson t-data new-contributor	56/12	Mathlib.lean,Mathlib/Data/Set/Lattice.lean,Mathlib/Data/Set/Pairwise/Chain.lean,Mathlib/Data/Set/Pairwise/Lattice.lean	4	11	['JasperMS', 'Ruben-VandeVelde', 'edegeltje', 'github-actions']	nobody	none	9-72336 9 days ago	12-40632 12 days ago	12-41075 12 days
28077	ShreckYe author:ShreckYe	feat(Data/Finset/Card): add some more Pigeonhole Principle theorems `exists_ne_map_eq_of_card_image_lt` and `not_injOn_of_card_image_lt`	`exists_ne_map_eq_of_card_image_lt` is a special case of `exists_ne_map_eq_of_card_lt_of_maps_to` where `t` is `s.image f`, and `not_injOn_of_card_image_lt` is its variant using `Set.InjOn`. I ran into some cases where such theorems would save me some time.	t-data new-contributor	10/0	Mathlib/Data/Finset/Card.lean	1	4	['ShreckYe', 'github-actions', 'themathqueen']	nobody	none	9-42125 9 days ago	13-53907 13 days ago	13-53955 13 days
28045	ShreckYe author:ShreckYe	feat(Data/Finset/Image): add `subset_univ_image_iff`	This is a special case of `subset_image_iff`, which corresponds to `Set.subset_range_iff_exists_image_eq` for `Set`.	t-data new-contributor	13/0	Mathlib/Data/Finset/Image.lean	1	2	['github-actions', 'themathqueen']	nobody	none	9-42020 9 days ago	14-38812 14 days ago	14-38874 14 days
28139	YaelDillies author:YaelDillies	refactor: make the cone explicit in `ConvexCone.toPointedCone`	Otherwise it is impossible to know which cone we are talking about from the infoview as proofs are elided. From Toric --- [](https://gitpod.io/from-referrer/)	t-convex-geometry toric maintainer-merge	3/3	Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean	2	2	['Ruben-VandeVelde', 'github-actions']	nobody	1	9-17613 9 days ago	9-17613 9 days ago	11-65907 11 days
28226	ShreckYe author:ShreckYe	feat(Data/Finset): `Multiset.eq_of_le_of_card_eq` and `Finset.eq_of_subet_of_card_eq`	As the conditions `s ⊆ t` for `Finset` and `s ≤ t` for `Multiset` both imply `card s ≤ card t`, the conditions `card t ≤ card s` in both `Finset.eq_of_subset_of_card_le` and `Multiset.eq_of_le_of_card_le` can be specialized to `card s = card t`, and due to this I'd argue `card s = card t` might be more common than `card t ≤ card s` in some cases. A similar theorem `Sublist.eq_of_length` for `Sublist` is already available in Lean. Adding these two theorems can aid proof search in such cases.	t-data new-contributor easy	6/0	Mathlib/Data/Finset/Card.lean,Mathlib/Data/Multiset/Defs.lean	2	3	['Ruben-VandeVelde', 'ShreckYe', 'github-actions']	nobody	none	8-62550 8 days ago	9-56242 9 days ago	9-56295 9 days
28241	alreadydone author:alreadydone	chore(Data): `SetLike Finset`	--- [](https://gitpod.io/from-referrer/)	t-data	54/62	Counterexamples/AharoniKorman.lean,Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean,Mathlib/Algebra/Module/FinitePresentation.lean,Mathlib/Combinatorics/Additive/RuzsaCovering.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean,Mathlib/Data/DFinsupp/Defs.lean,Mathlib/Data/Finset/Defs.lean,Mathlib/Data/Finset/Insert.lean,Mathlib/Data/Finset/Union.lean,Mathlib/FieldTheory/Perfect.lean,Mathlib/GroupTheory/Perm/Centralizer.lean,Mathlib/GroupTheory/Perm/Cycle/Basic.lean,Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean,Mathlib/LinearAlgebra/Finsupp/Supported.lean,Mathlib/LinearAlgebra/LinearIndependent/Basic.lean,Mathlib/LinearAlgebra/LinearIndependent/Defs.lean,Mathlib/MeasureTheory/Integral/IntegrableOn.lean,Mathlib/ModelTheory/Semantics.lean,Mathlib/Order/CountableDenseLinearOrder.lean,Mathlib/Probability/Independence/Kernel.lean,Mathlib/RingTheory/Ideal/Quotient/Index.lean,Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean,Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean,Mathlib/Topology/Separation/Basic.lean	25	1	['github-actions']	nobody	none	8-52994 8 days ago	8-52994 8 days ago	8-52978 8 days
28242	robin-carlier author:robin-carlier	feat(CategoryTheory/Bicategory): EqToHom for bicategories	We generalize the `eqToHom` construction from `Category` to `CategoryStruct`, allowing its usage in bicategorical contexts. We introduce a file `CategoryTheory/Bicategory/EqToHom` that records some of the properties of `eqToHom`s 1-morphisms and 2-morphisms, such as the transitivity up to isomorphism of `eqToHom` 1-morphisms, and congruence lemmas for unitors, associators and whiskering with respects to `eqToHom` 2-morphisms. This generalization and these congruence lemmas will be used to define icons between lax functors, and work with categories of strictly unitary lax/pseudo-functors (e.g for pseudocomposable arrows and lax-composable arrows in bicategories, which are part of the definitions of nerve constructions in bicategories). --- A follow-up PR will move some existing `eqToHom`-related lemmas from `CategoryTheory/Bicategory/Strict` to this new file. [](https://gitpod.io/from-referrer/)	t-category-theory	150/4	Mathlib.lean,Mathlib/CategoryTheory/Bicategory/EqToHom.lean,Mathlib/CategoryTheory/EqToHom.lean	3	1	['github-actions']	nobody	none	8-49436 8 days ago	8-49443 8 days ago	9-39328 9 days
27634	agjftucker author:agjftucker	fix(Analysis/Calculus/Implicit): consistently rename {`map`, `fun`, `function`} to `fun`	There are several clear naming issues in the file Implicit.lean, such as ``` theorem prod_map_implicitFunction : ∀ᶠ p : F × G in 𝓝 (φ.prodFun φ.pt), φ.prodFun (φ.implicitFunction p.1 p.2) = p := ``` where `prod_map` and `prodFun` both refer to the same thing. In this PR I have done my best to resolve these as consistently as possible by renaming everything `map`, also everything `function`, to `fun`. This has the added benefit of making some long names a little shorter. In passing I rewrapped some comments and replaced `haveI` with `have` where it had been used like `haveI` in Lean 3. Moves: - ImplicitFunctionData -> ImplicitFunData - ImplicitFunctionData.implicitFunction -> ImplicitFunData.implicitFun - ImplicitFunctionData.prod_map_implicitFunction -> ImplicitFunData.prodFun_implicitFun - ImplicitFunctionData.left_map_implicitFunction -> ImplicitFunData.leftFun_implicitFun - ImplicitFunctionData.right_map_implicitFunction -> ImplicitFunData.rightFun_implicitFun - ImplicitFunctionData.implicitFunction_apply_image -> ImplicitFunData.implicitFun_apply_image - ImplicitFunctionData.implicitFunction_hasStrictFDerivAt -> ImplicitFunData.hasStrictFDerivAt_implicitFun - HasStrictFDerivAt.implicitFunctionDataOfComplemented -> HasStrictFDerivAt.implicitFunDataOfComplemented - HasStrictFDerivAt.implicitFunctionOfComplemented -> HasStrictFDerivAt.implicitFunOfComplemented - HasStrictFDerivAt.map_implicitFunctionOfComplemented_eq -> HasStrictFDerivAt.map_implicitFunOfComplemented_eq - HasStrictFDerivAt.eq_implicitFunctionOfComplemented -> HasStrictFDerivAt.eq_implicitFunOfComplemented - HasStrictFDerivAt.implicitFunctionOfComplemented_apply_image -> HasStrictFDerivAt.implicitFunOfComplemented_apply_image - HasStrictFDerivAt.to_implicitFunctionOfComplemented -> HasStrictFDerivAt.to_implicitFunOfComplemented - HasStrictFDerivAt.implicitFunction -> HasStrictFDerivAt.implicitFun - HasStrictFDerivAt.tendsto_implicitFunction -> HasStrictFDerivAt.tendsto_implicitFun - _root_.Filter.Tendsto.implicitFunction -> _root_.Filter.Tendsto.implicitFun - HasStrictFDerivAt.map_implicitFunction_eq -> HasStrictFDerivAt.map_implicitFun_eq - HasStrictFDerivAt.implicitFunction_apply_image -> HasStrictFDerivAt.implicitFun_apply_image - HasStrictFDerivAt.eq_implicitFunction -> HasStrictFDerivAt.eq_implicitFun - HasStrictFDerivAt.to_implicitFunction -> HasStrictFDerivAt.to_implicitFun --- [](https://gitpod.io/from-referrer/)	t-analysis	165/121	Mathlib/Analysis/Calculus/Implicit.lean,docs/1000.yaml,docs/overview.yaml,docs/undergrad.yaml	4	1	['github-actions']	nobody	none	8-31858 8 days ago	8-31859 8 days ago	22-48445 22 days
26192	kckennylau author:kckennylau	feat(LinearAlgebra): symmetric tensor power	This file defines the symmetric tensor power of a module over a ring. The finite powers will form a grading of the symmetric algebra. The n-th symmetric R-tensor power of M will also correspond to global sections of a line bundle on Proj(M) of degree n. It also has a universal property where maps out of it correspond to symmetric multilinear forms. --- Zulip: [#mathlib4 > Proposal: Symmetric Tensor Power](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Proposal.3A.20Symmetric.20Tensor.20Power/with/524795235) [](https://gitpod.io/from-referrer/)	t-algebra label:t-algebra$	137/0	Mathlib.lean,Mathlib/LinearAlgebra/TensorPower/Symmetric.lean	2	12	['AntoineChambert-Loir', 'erdOne', 'eric-wieser', 'github-actions', 'kckennylau', 'mattrobball']	nobody	none	8-30864 8 days ago	9-64137 9 days ago	59-12912 59 days
28321	kim-em author:kim-em	chore: make OmegaCompletePartialOrder a mixin	I've noted typeclass searches often getting distracted looking for a `OmegaCompletePartialOrder` when they just want an `LE` or a `Preorder`. Let's benchmark to see it if has a nontrivial effect. Not certain if this is desirable if the performance change is neutral (or even negative).		68/43	Mathlib/Control/LawfulFix.lean,Mathlib/Data/Nat/Nth.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean,Mathlib/Order/Category/OmegaCompletePartialOrder.lean,Mathlib/Order/OmegaCompletePartialOrder.lean,Mathlib/Topology/OmegaCompletePartialOrder.lean	6	4	['github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot']	nobody	none	7-74040 7 days ago	7-74040 7 days ago	7-83994 7 days
28292	bwangpj author:bwangpj	feat(Geometry/Manifold/ContMDiff): add product lemmas for `ContMDiff`	Add product lemmas for `ContMDiff`. These are analogous to the corresponding lemmas for `Continuous` in [`Mathlib.Topology.Constructions.SumProd`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Constructions/SumProd.html#ContinuousAt.comp%E2%82%82). This is upstreamed from [https://github.com/girving/ray](https://github.com/girving/ray). Co-authored-by: Geoffrey Irving --- [](https://gitpod.io/from-referrer/)	new-contributor	42/0	Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean	1	1	['github-actions']	nobody	none	7-72553 7 days ago	8-39258 8 days ago	8-39251 8 days
27552	Equilibris author:Equilibris	refactor: make universe levels visible in typevec	This will be needed to allow `M.corec` to be generic across universes --- [](https://gitpod.io/from-referrer/)	t-data new-contributor easy	16/10	Mathlib/Data/TypeVec.lean	1	9	['Equilibris', 'eric-wieser', 'github-actions', 'plp127']	nobody	1	7-68981 7 days ago	8-21400 8 days ago	24-33920 24 days
28150	Equilibris author:Equilibris	chore: clean up proofs typevec proofs	While adding variable universe corecs I found a lot of theorems in typevec that could do with a bit of a clean-up --- [](https://gitpod.io/from-referrer/)	t-data new-contributor	24/26	Mathlib/Data/TypeVec.lean	1	6	['Equilibris', 'alexkeizer', 'github-actions']	nobody	1	7-61029 7 days ago	7-61029 7 days ago	11-56627 11 days
28185	Sebi-Kumar author:Sebi-Kumar	feat(Topology/Path): add theorem about casting with rfl	Prove the trivial result `p.cast rfl rfl = p` for a path `p`, which serves as a useful result for the simplifier to know. Suggested by Aaron Liu at the discussion [#Is there code for X? > Dealing with `Path.cast`](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Dealing.20with.20.60Path.2Ecast.60). --- To provide additional context, I am relatively new when it comes to contributing to Mathlib, and I am doing so as a part of the Fields Undergraduate Summer Research Program hosted at the University of Western Ontario under the supervision of Chris Kapulkin and Daniel Carranza. My goal is to contribute that the `n`-sphere is simply connected for `n > 1`. [](https://gitpod.io/from-referrer/)	new-contributor t-topology easy	2/0	Mathlib/Topology/Path.lean	1	1	['github-actions', 'kckennylau', 'plp127']	nobody	2	7-42014 7 days ago	7-42014 7 days ago	10-34138 10 days
28325	pechersky author:pechersky	feat(WithZeroTopology): `locallyCompactSpace_iff_locallyFiniteOrder_units`	On the way to golf/generalize the proof that locally compact valued fields have locally finite valuation groups as embodied in `Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer` ] --- [](https://gitpod.io/from-referrer/)	large-import t-order t-topology	160/2	Mathlib/Topology/Algebra/GroupWithZero.lean,Mathlib/Topology/Algebra/WithZeroTopology.lean,Mathlib/Topology/Compactness/Compact.lean	3	1	['github-actions']	nobody	none	7-39214 7 days ago	7-70032 7 days ago	7-72742 7 days
28350	themathqueen author:themathqueen	feat(Topology/Algebra/Module/LinearMap): `range (f.smulRight x) = span {x}`	--- [](https://gitpod.io/from-referrer/)	t-algebra t-topology label:t-algebra$	14/0	Mathlib/Topology/Algebra/Module/LinearMap.lean	1	2	['github-actions', 'themathqueen']	nobody	none	7-32200 7 days ago	7-33508 7 days ago	7-36099 7 days
28337	joelriou author:joelriou	feat(AlgebraicTopology): nondegenerate simplices in the nerve of a partially ordered type	In this PR, we show that nondegenerate simplices in the nerve of a partially ordered type `X` correspond to strictly monotone functions `Fin (n + 1) → X`. (Incidentally, better normal formal are used for the RHS of lemmas involving (non)degenerate simplices of dimension `0`.) --- [](https://gitpod.io/from-referrer/)	t-algebraic-topology	102/11	Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialNerve.lean,Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean,Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean,Mathlib/AlgebraicTopology/SimplicialSet/NerveNondegenerate.lean	5	1	['github-actions']	nobody	none	7-25743 7 days ago	7-53226 7 days ago	7-53210 7 days
28182	themathqueen author:themathqueen	feat(Data/Matrix/Basis): `center (Matrix n n α) = scalar n '' center α`	The center of `Matrix n n α` is trivial for semiring `α`. --- [](https://gitpod.io/from-referrer/)	t-data	39/13	Mathlib/Algebra/Central/Matrix.lean,Mathlib/Data/Matrix/Basis.lean	2	37	['eric-wieser', 'github-actions', 'kckennylau', 'themathqueen']	nobody	none	7-23496 7 days ago	10-39494 10 days ago	10-39539 10 days
25292	YaelDillies author:YaelDillies	feat: the `ConvexCone` generated by a set	Define `ConvexCone.copy` and `ConvexCone.hull` and use them to golf the `CompleteLattice` instance. From Toric --- - [x] depends on: #25291 [](https://gitpod.io/from-referrer/)	t-convex-geometry toric	94/35	Mathlib/Analysis/Convex/Cone/Basic.lean,Mathlib/Geometry/Convex/Cone/Basic.lean	2	8	['YaelDillies', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot']	nobody	none	7-20436 7 days ago	24-53377 24 days ago	62-5304 62 days
27390	alreadydone author:alreadydone	feat(FieldTheory/Galois): normal basis theorem	Co-authored-by: Madison Crim @maddycrim Co-authored-by: Aaron Liu @plp127 Co-authored-by: Justus Springer @justus-springer from [*Formalizing Class Field Theory*](https://www.claymath.org/events/formalizing-class-field-theory/) --- - [x] depends on: #27355 - [x] depends on: #27368 [](https://gitpod.io/from-referrer/)	t-algebra label:t-algebra$	156/1	Mathlib.lean,Mathlib/Algebra/Module/PID.lean,Mathlib/Algebra/Polynomial/Module/AEval.lean,Mathlib/FieldTheory/Galois/NormalBasis.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/LinearAlgebra/LinearIndependent/Basic.lean,docs/references.bib	7	2	['github-actions', 'mathlib4-dependent-issues-bot']	nobody	none	7-16300 7 days ago	7-18088 7 days ago	7-18071 7 days
27842	alreadydone author:alreadydone	chore(MonoidLocalization): get rid of Submonoid.LocalizationWithZeroMap	because every `Submonoid.LocalizationMap` automatically preserves zero. Also removes a condition from `isLeftRegular_of_le_isCancelMulZero` by proving `map_isRegular`, which is used to prove other related lemmas. `toMap_injective_iff` is moved from MonoidWithZero.lean to Basic.lean. --- `Submonoid.LocalizationMap` could potentially be made a FunLike and MonoidWithZeroHomClass, but it's also reasonable (and maybe useful) to unbundle it and use the same predicate as `IsLocalization`. - [x] depends on: #27791 [](https://gitpod.io/from-referrer/)	t-algebra label:t-algebra$	81/98	Mathlib/GroupTheory/MonoidLocalization/Basic.lean,Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean,Mathlib/RingTheory/Localization/Defs.lean,Mathlib/RingTheory/OrderOfVanishing.lean	4	2	['github-actions', 'mathlib4-dependent-issues-bot']	nobody	none	7-15785 7 days ago	18-5740 18 days ago	18-5724 18 days
26988	YaelDillies author:YaelDillies	feat(Rel): more API	Some of this API already exists in `Topology.UniformSpace.Defs` but not spelled with `SetRel`, some of it was written for #24173. --- `Topology.UniformSpace.Defs` will be refactored to use these new lemmas in #23181. [](https://gitpod.io/from-referrer/)	t-data	179/8	Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Data/Rel.lean	2	2	['github-actions', 'mathlib4-merge-conflict-bot']	nobody	none	6-53453 6 days ago	7-68864 7 days ago	40-43104 40 days
28220	kim-em author:kim-em	chore: cleanup three #adaptation_notes	--- [](https://gitpod.io/from-referrer/)	maintainer-merge	5/26	Mathlib/Data/Bool/Basic.lean,Mathlib/Logic/Function/Defs.lean,Mathlib/Tactic/NormNum/Pow.lean	3	6	['bryangingechen', 'github-actions', 'grunweg', 'kim-em', 'mathlib4-merge-conflict-bot']	nobody	none	6-52008 6 days ago	7-6504 7 days ago	9-22406 9 days
28356	JovanGerb author:JovanGerb	chore(Data/Rat/Cast/CharZero): rename `Rat.cast_mk` to `Rat.cast_divInt`	The symbol `/.` is notation for `Rat.divInt`, not `Rat.mk`, so this PR renames `Rat.cast_mk` to `Rat.cast_divInt`. --- [](https://gitpod.io/from-referrer/)	t-data	5/3	Mathlib/Data/Rat/Cast/CharZero.lean,Mathlib/Data/Rat/Defs.lean,Mathlib/Data/Real/Irrational.lean	3	1	['github-actions']	nobody	none	6-47552 6 days ago	7-21351 7 days ago	7-21397 7 days
28312	LLaurance author:LLaurance	feat(Combinatorics/SimpleGraph): minimum degree of nontrivial tree is one	Add basic facts about nontrivial preconnected SimpleGraphs and that a nontrivial tree has a vertex of degree one. The motivation for this is to ultimately show that any connected graph contains a vertex that, when removed, leaves the graph connected. Any connected graph has a spanning tree which contains a vertex of degree one that fulfils the role of the vertex to be removed. --- [](https://gitpod.io/from-referrer/)	large-import new-contributor t-combinatorics	33/2	Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean	2	6	['LLaurance', 'eric-wieser', 'github-actions']	nobody	none	6-31087 6 days ago	8-8948 8 days ago	8-17086 8 days
27163	pechersky author:pechersky	feat(Topology/ValuativeRel): of and to basis of compatible valuations	--- [](https://gitpod.io/from-referrer/)	t-algebra t-topology t-number-theory label:t-algebra$	205/25	Mathlib/RingTheory/Valuation/ValuativeRel.lean,Mathlib/Topology/Algebra/Valued/ValuativeRel.lean	2	26	['github-actions', 'kckennylau', 'mathlib4-merge-conflict-bot', 'pechersky']	nobody	none	5-78845 5 days ago	7-34404 7 days ago	36-14723 36 days
26588	faenuccio author:faenuccio	feat(Algebra/GroupWithZero/WithZero): add the multiplicative embedding with zero from the range	We extend the embedding of the range of a `MonoidWithZeroHom` to the codomain by enriching it with the strucutre of an ordered, multiplicative embedding. In passing, we extend some results about the embedding of `WithZero` of the units of a group with zero, to the group itself. Co-authored by: María Inés de Frutos Fernández @mariainesdff --- [](https://gitpod.io/from-referrer/)	t-order t-algebra label:t-algebra$	145/10	Mathlib.lean,Mathlib/Algebra/GroupWithZero/Range.lean,Mathlib/Algebra/GroupWithZero/WithZero.lean,Mathlib/Algebra/Order/GroupWithZero/Range.lean,Mathlib/Algebra/Order/GroupWithZero/WithZero.lean,Mathlib/Algebra/Order/Monoid/WithTop.lean	6	27	['faenuccio', 'github-actions', 'leanprover-community-bot-assistant', 'pechersky']	nobody	none	5-34459 5 days ago	7-41846 7 days ago	12-61933 12 days
28286	bwangpj author:bwangpj	feat(Geometry/Manifold/ContMDiff): basic lemmas for analytic (`C^ω`) functions	Add basic lemmas relating `ContMDiff` in the `C^ω` case to being `Analytic` on charts. This is upstreamed from [https://github.com/girving/ray](https://github.com/girving/ray). Co-authored-by: Geoffrey Irving --- [](https://gitpod.io/from-referrer/)	new-contributor t-differential-geometry	36/0	Mathlib/Geometry/Manifold/ContMDiff/Defs.lean	1	2	['girving', 'github-actions']	nobody	none	3-52103 3 days ago	8-50442 8 days ago	8-50487 8 days
28338	themathqueen author:themathqueen	feat(Analysis/InnerProductSpace/IsPositive): `(adjoint S ∘ S).IsPositive` and `(S ∘ adjoint S).IsPositive`	--- [](https://gitpod.io/from-referrer/)	t-analysis easy	16/0	Mathlib/Analysis/InnerProductSpace/Positive.lean	1	1	['github-actions']	nobody	none	2-40145 2 days ago	7-52687 7 days ago	7-52691 7 days
27973	smmercuri author:smmercuri	feat: the ring of integers of a `ℤₘ₀`-valued field is compact whenever it is a DVR and the residue field is finite	This PR continues the work from #21844. Original PR: https://github.com/leanprover-community/mathlib4/pull/21844	large-import	54/2	Mathlib/RingTheory/Ideal/Quotient/Basic.lean,Mathlib/Topology/Algebra/Valued/WithZeroMulInt.lean	2	1	['github-actions']	nobody	none	1-51374 1 day ago	8-31717 8 days ago	8-31732 8 days
28316	eric-wieser author:eric-wieser	feat(Tactic/NormNum): better trace nodes	Comparing the infoview on the first example in the test file | Before | After | |---|---| | | | In the after version, the extension names are all clickable. Similar to #21450. --- [](https://gitpod.io/from-referrer/)	t-meta	138/5	Mathlib.lean,Mathlib/Tactic/NormNum/Core.lean,Mathlib/Util/Trace.lean,MathlibTest/norm_num_trace.lean	4	6	['eric-wieser', 'github-actions', 'leanprover-bot', 'plp127']	nobody	none	1-4924 1 day ago	8-9505 8 days ago	8-9494 8 days
19872	YaelDillies author:YaelDillies	chore(GroupTheory/Index): rename `relindex` to `relIndex`	Zulip discussion about renaming: [#PR reviews > #19872 rename relindex to relIndex @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2319872.20rename.20relindex.20to.20relIndex/near/515908054) --- - [x] depends on: #24044 [](https://gitpod.io/from-referrer/)	FLT maintainer-merge t-algebra label:t-algebra$	288/182	Mathlib/Algebra/Module/ZLattice/Covolume.lean,Mathlib/FieldTheory/Relrank.lean,Mathlib/GroupTheory/Commensurable.lean,Mathlib/GroupTheory/CosetCover.lean,Mathlib/GroupTheory/GroupAction/Blocks.lean,Mathlib/GroupTheory/Index.lean,Mathlib/GroupTheory/IndexNormal.lean,Mathlib/GroupTheory/PGroup.lean,Mathlib/GroupTheory/Schreier.lean,Mathlib/GroupTheory/SchurZassenhaus.lean,Mathlib/GroupTheory/Sylow.lean,Mathlib/GroupTheory/Transfer.lean,Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean,Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean,Mathlib/NumberTheory/NumberField/Discriminant/Different.lean,Mathlib/NumberTheory/NumberField/Units/Regulator.lean,Mathlib/RingTheory/Ideal/Quotient/Index.lean	17	27	['Ruben-VandeVelde', 'TwoFX', 'YaelDillies', 'alreadydone', 'eric-wieser', 'github-actions', 'kbuzzard', 'leanprover-community-bot-assistant', 'loefflerd', 'madvorak', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'tb65536']	nobody	1	0-60235 16 hours ago	7-55242 7 days ago	200-68756 200 days
26330	Timeroot author:Timeroot	"Junk value" test file	This PR continues the work from #25173. Original PR: https://github.com/leanprover-community/mathlib4/pull/25173	t-data	360/0	MathlibTest/Junk.lean	1	3	['Timeroot', 'github-actions', 'leanprover-community-bot-assistant']	nobody	none	0-39438 10 hours ago	41-17920 1 month ago	56-66802 56 days
26331	Timeroot author:Timeroot	feat(Algebra/Polynomial): Descartes' Rule of signs	This PR continues the work from #23681. Original PR: https://github.com/leanprover-community/mathlib4/pull/23681	t-algebra label:t-algebra$	616/3	Mathlib.lean,Mathlib/Algebra/Polynomial/CoeffList.lean,Mathlib/Algebra/Polynomial/Degree/Operations.lean,Mathlib/Algebra/Polynomial/EraseLead.lean,Mathlib/Algebra/Polynomial/RuleOfSigns.lean	5	5	['Timeroot', 'adomani', 'github-actions']	nobody	none	0-28801 8 hours ago	57-80551 1 month ago	57-80595 57 days
27212	CBirkbeck author:CBirkbeck	Cot series iterated deriv within	--- - [x] depends on: #27209 - [x] depends on: #26016 [](https://gitpod.io/from-referrer/)		237/2	Mathlib/Analysis/Complex/IntegerCompl.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean	4	4	['github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot']	nobody	none	0-28279 7 hours ago	8-57621 8 days ago	8-71582 8 days
25899	pfaffelh author:pfaffelh	feat(Topology/Compactness/CompactSystem): introduce compact Systems	A compact system is a set systems with the property that, whenever a countable intersections of sets in the set system is empty, there is a finite subset of sets with empty intersection. These are needed e.g. in measure theory if one wants to show sigma-additivity of a set function on a ring. * Main result: The set of sets which are either compact and closed, or `univ`, is a compact system. * Introduce `Dissipate s x := ⋂ y ≤ x, s y` (Data/Set/Dissipate), which is parallel to Data/Set/Accumulate. Co-authored-by: Rémy Degenne remydegenne@gmail.com --- *This PR continues the work from #24541.* *Original PR: https://github.com/leanprover-community/mathlib4/pull/24541*	t-topology	471/14	Mathlib.lean,Mathlib/Data/Set/Accumulate.lean,Mathlib/Data/Set/Dissipate.lean,Mathlib/MeasureTheory/PiSystem.lean,Mathlib/Topology/Compactness/CompactSystem.lean	5	13	['github-actions', 'pfaffelh', 'sgouezel']	nobody	none	0-18139 5 hours ago	25-38544 25 days ago	41-10608 41 days
25794	dagurtomas author:dagurtomas	feat(CategoryTheory): localization preserves braided structure	--- [](https://gitpod.io/from-referrer/) --- *This PR continues the work from #24485.* *Original PR: https://github.com/leanprover-community/mathlib4/pull/24485*	file-removed t-category-theory	733/427	Mathlib.lean,Mathlib/CategoryTheory/Localization/Monoidal.lean,Mathlib/CategoryTheory/Localization/Monoidal/Basic.lean,Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean,Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Sites/Monoidal.lean	6	2	['github-actions', 'leanprover-community-bot-assistant']	nobody	none	0-15519 4 hours ago	46-75991 1 month ago	22-63640 22 days
26120	vasnesterov author:vasnesterov	feat(Data/Seq): `update` and `set` operations for `Seq`	Introduce `modify` and `set` operations for sequences, along with a few lemmas about them. --- - [x] depends on: #20071 [](https://gitpod.io/from-referrer/) This PR continues the work from #20160. Original PR: https://github.com/leanprover-community/mathlib4/pull/20160	t-data	69/0	Mathlib/Data/Seq/Seq.lean	1	4	['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'vasnesterov']	nobody	none	0-15023 4 hours ago	63-20340 2 months ago	63-20390 63 days
26738	javra author:javra	feat(AlgebraicToplogy/SimplexCategory): add notation for faces and degeneracies general truncated simplex categories	--- [](https://gitpod.io/from-referrer/)	t-algebraic-topology infinity-cosmos	43/32	Mathlib/AlgebraicTopology/SimplexCategory/Truncated.lean,Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean	2	4	['emilyriehl', 'github-actions', 'leanprover-community-bot-assistant']	nobody	none	0-1452 24 minutes ago	19-47751 19 days ago	33-38754 33 days
26829	pechersky author:pechersky	feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodule versions of ltAddSubgroup	Extracted from #25450 without changing how Valued works --- [](https://gitpod.io/from-referrer/) @faenuccio hopefully this bypasses any wait on #14752 because I am not changing Valued files.	t-ring-theory	172/0	Mathlib/RingTheory/Valuation/Basic.lean,Mathlib/RingTheory/Valuation/Integers.lean	2	3	['JovanGerb', 'github-actions', 'mathlib4-merge-conflict-bot']	nobody	none	0-1451 24 minutes ago	12-23774 12 days ago	44-84694 44 days
27244	xroblot author:xroblot	feat(RingTheory/DedekindDomain): lifting an ideal in an extension is injective	This PR develops some API for [FractionalIdeal.extended](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/FractionalIdeal/Extended.html#FractionalIdeal.extended) and in particular for when it is an injective map (for an algebra map). As a consequence, it deduces the fact that lifting an integral ideal in an extension of Dedekind domains is an injective map. Note: the import increase happens in a leaf file `Mathlib.RingTheory.FractionalIdeal.Extended` --- [](https://gitpod.io/from-referrer/)	t-ring-theory large-import	190/5	Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean,Mathlib/RingTheory/FractionalIdeal/Extended.lean,Mathlib/RingTheory/Localization/Basic.lean	3	2	['github-actions', 'leanprover-community-bot-assistant']	nobody	none	0-1450 24 minutes ago	16-27816 16 days ago	33-53809 33 days
27657	euprunin author:euprunin	chore(Geometry/RingedSpace): remove use of `erw` in `forget_preservesLimitsOfLeft`		t-algebraic-geometry	5/2	Mathlib/Geometry/RingedSpace/OpenImmersion.lean	1	1	['github-actions']	nobody	none	0-1450 24 minutes ago	22-10020 22 days ago	22-10067 22 days
27992	staroperator author:staroperator	feat(Algebra): cancellation inheritance	This PR: 1. adds `Is{Left,Right}Cancel{Add,Mul,MulZero}` instances for `{Add,Mul,MulZero}MemClass` etc. 2. duplicates such instances for `Subsemiring` and `Subalgebra`, following #27955 (which is for `Submonoid` and `Submodule`). --- [](https://gitpod.io/from-referrer/)	t-algebra label:t-algebra$	74/1	Mathlib.lean,Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Group/Submonoid/Defs.lean,Mathlib/Algebra/Group/Subsemigroup/Defs.lean,Mathlib/Algebra/GroupWithZero/Submonoid/CancelMulZero.lean,Mathlib/Algebra/Module/Submodule/Defs.lean,Mathlib/Algebra/Ring/Subsemiring/Defs.lean	7	7	['Vierkantor', 'eric-wieser', 'github-actions', 'mathlib4-merge-conflict-bot', 'staroperator']	nobody	none	0-1449 24 minutes ago	9-10107 9 days ago	15-20274 15 days
28124	kckennylau author:kckennylau	feat(Tactic): Call an arbitrary Simproc	In the current framework, `Simproc`s are declared by name, and can only be referred to by name. For example, [Nat.divisors_ofNat](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Simproc/Divisors.html#Nat.divisors_ofNat) is declared as: ```lean dsimproc_decl Nat.divisors_ofNat (Nat.divisors _) := fun e => do ``` This declaration syntax does not allow for a `Simproc` to depend on any arguments, and even if one constructed a `Simproc` that depends on e.g. a natural number, such as `foo : ℕ → Simproc`, one still cannot call it using the syntax `by simp [foo 37]`. Therefore, this new function aims to solve this problem, by allowing an arbitrary `Simproc` to be executed, using the newly defined function `Lean.Meta.Simp.Simproc.apply (s : Simproc) : TacticM Unit`. --- [](https://gitpod.io/from-referrer/)	t-meta	99/0	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Simproc/Apply.lean,MathlibTest/Simproc/Apply.lean	4	12	['b-mehta', 'eric-wieser', 'github-actions', 'hrmacbeth', 'kckennylau']	nobody	none	0-1448 24 minutes ago	12-9325 12 days ago	12-19525 12 days
28329	pechersky author:pechersky	feat(RingTheory/Valuation): generalize CommGroupWithZero on mrange to MonoidWithZeroHom	Before, they were only for Valuation, but that is too restricted --- [](https://gitpod.io/from-referrer/)	t-ring-theory t-order t-algebra label:t-algebra$	21/4	Mathlib/RingTheory/Valuation/Archimedean.lean,Mathlib/RingTheory/Valuation/Basic.lean	2	3	['eric-wieser', 'github-actions', 'pechersky']	nobody	none	0-1446 24 minutes ago	7-70019 7 days ago	7-70065 7 days
28287	robin-carlier author:robin-carlier	chore(CategoryTheory/Bicategory): move `map₂_eqToHom` earlier in the import graph	The lemma `PrelaxFunctor.map₂_eqToHom` currently sits in the file `CategoryTheory/Bicategory/LocallyDiscrete`. This has low discoverability, and it is unavailable to other files that deals with `eqToHoms`, such as `CategoryTheory/Bicategory/Functor/Strict`. We move the lemma in the file `Category/Bicategory/Functor/Prelax`. This comes at the cost of an extra import (`CategoryTheory.EqToHom`) in the file. The lemma is unsimped for consistency with the corresponding lemma for ordinary categories, which is intentionally not a simp lemma. We also sneak in the `eqToIso` version for completeness. --- Feel free to disagree with the extra import. I think putting this lemma closer to the definition of prelax functors is what makes most sense. An other possible home for this lemma is the file `CategoryTheory/Bicategory/EqToHom` that I introduce in #28242, but this would require that it imports prelax functors. [](https://gitpod.io/from-referrer/)	large-import t-category-theory	13/12	Mathlib/CategoryTheory/Bicategory/Functor/Prelax.lean,Mathlib/CategoryTheory/Bicategory/Grothendieck.lean,Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean,Mathlib/CategoryTheory/FiberedCategory/Grothendieck.lean	4	1	['github-actions']	nobody	none	0-1446 24 minutes ago	8-48462 8 days ago	8-48978 8 days
28352	agjftucker author:agjftucker	feat(Analysis): add three little theorems relating argument to image	These relate argument to image under a continuous function, given a Prop that eventually holds on a product of filters in domain and codomain. In fact the second pair of statements concern a segment whose end-points are the image. They should prove useful in PRs 26300 and 26985. --- [](https://gitpod.io/from-referrer/)	t-analysis	28/3	Mathlib/Analysis/Normed/Module/Convex.lean,Mathlib/Order/Filter/Prod.lean	2	1	['github-actions']	nobody	none	0-1445 24 minutes ago	7-26148 7 days ago	7-33339 7 days

Stale assigned PRs on the review queue