Maintainers page: short tasks

Are you a maintainer with just a short amount of time? The following kinds of pull requests could be relevant for you.

If you realise you actually have a bit more time, you can also look at the page for reviewers, or look at the triage page!
This dashboard was last updated on: November 14, 2025 at 08:16 UTC

Stale ready-to-merge'd PRs

There are currently no stale PRs labelled auto-merge-after-CI or ready-to-merge. Congratulations!

Stale maintainer-merge'd PRs

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
30047 ooovi
author:ooovi
 feat(Combinatorics/SimpleGraph): edge labellings Add edge labellings for `SimpleGraph` as well as some basic lemmata. --- This is mostly a cleaned up part of @b-mehta's lean4 port of their [formalisation of an exponentially better upper bound on Ramsey numbers ](https://github.com/b-mehta/ExponentialRamsey/). I need these definitions for another project on Ramsey theory. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-combinatorics awaiting-author 234/3 Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/EdgeLabelling.lean,Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean,Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean 5 52 ['YaelDillies', 'b-mehta', 'github-actions', 'ooovi', 'vlad902'] b-mehta
assignee:b-mehta
6-8643
6 days ago
10-1364
10 days ago
34-69915
34 days
31201 euprunin
author:euprunin
 chore(RingTheory): golf `isPrimary_decomposition_pairwise_ne_radical` using `grind` ---
Show trace profiling of isPrimary_decomposition_pairwise_ne_radical: 89 ms before, 156 ms after ### Trace profiling of `isPrimary_decomposition_pairwise_ne_radical` before PR 31201 ```diff diff --git a/Mathlib/RingTheory/Lasker.lean b/Mathlib/RingTheory/Lasker.lean index 8f522d48f8..21bf4d68b6 100644 --- a/Mathlib/RingTheory/Lasker.lean +++ b/Mathlib/RingTheory/Lasker.lean @@ -57,6 +57,7 @@ lemma decomposition_erase_inf [DecidableEq (Ideal R)] {I : Ideal R} open scoped Function -- required for scoped `on` notation +set_option trace.profiler true in lemma isPrimary_decomposition_pairwise_ne_radical {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) : ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧ ``` ``` ℹ [1261/1261] Built Mathlib.RingTheory.Lasker (1.3s) info: Mathlib/RingTheory/Lasker.lean:61:0: [Elab.command] [0.013044] theorem isPrimary_decomposition_pairwise_ne_radical {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) : ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧ (t : Set (Ideal R)).Pairwise ((· ≠ ·) on radical) := by classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · rw [← hs] refine le_antisymm ?_ ?_ <;> intro x hx · simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl · simp only [Submodule.mem_finsetInf, id_eq, Finset.inf_image, CompTriple.comp_eq, Function.comp_apply, Finset.mem_filter, and_imp] at hx ⊢ intro J _ K hK _ exact hx K hK · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.definition.header] [0.010071] Ideal.isPrimary_decomposition_pairwise_ne_radical info: Mathlib/RingTheory/Lasker.lean:61:0: [Elab.command] [0.016459] lemma isPrimary_decomposition_pairwise_ne_radical {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) : ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧ (t : Set (Ideal R)).Pairwise ((· ≠ ·) on radical) := by classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · rw [← hs] refine le_antisymm ?_ ?_ <;> intro x hx · simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl · simp only [Submodule.mem_finsetInf, id_eq, Finset.inf_image, CompTriple.comp_eq, Function.comp_apply, Finset.mem_filter, and_imp] at hx ⊢ intro J _ K hK _ exact hx K hK · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] info: Mathlib/RingTheory/Lasker.lean:61:0: [Elab.async] [0.091697] elaborating proof of Ideal.isPrimary_decomposition_pairwise_ne_radical [Elab.definition.value] [0.089099] Ideal.isPrimary_decomposition_pairwise_ne_radical [Elab.step] [0.086924] classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · rw [← hs] refine le_antisymm ?_ ?_ <;> intro x hx · simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl · simp only [Submodule.mem_finsetInf, id_eq, Finset.inf_image, CompTriple.comp_eq, Function.comp_apply, Finset.mem_filter, and_imp] at hx ⊢ intro J _ K hK _ exact hx K hK · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.086918] classical [… 154 lines omitted …] Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl · simp only [Submodule.mem_finsetInf, id_eq, Finset.inf_image, CompTriple.comp_eq, Function.comp_apply, Finset.mem_filter, and_imp] at hx ⊢ intro J _ K hK _ exact hx K hK [Elab.step] [0.020717] rw [← hs] refine le_antisymm ?_ ?_ <;> intro x hx · simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl · simp only [Submodule.mem_finsetInf, id_eq, Finset.inf_image, CompTriple.comp_eq, Function.comp_apply, Finset.mem_filter, and_imp] at hx ⊢ intro J _ K hK _ exact hx K hK [Elab.step] [0.010102] · simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl [Elab.step] [0.010064] simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl [Elab.step] [0.010060] simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl [Elab.step] [0.015365] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] [Elab.step] [0.015273] simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] [Elab.step] [0.015268] simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] [Elab.step] [0.027960] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.027947] intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.027944] intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.014324] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.014317] rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.014310] rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] Build completed successfully (1261 jobs). ``` ### Trace profiling of `isPrimary_decomposition_pairwise_ne_radical` after PR 31201 ```diff diff --git a/Mathlib/RingTheory/Lasker.lean b/Mathlib/RingTheory/Lasker.lean index 8f522d48f8..6f1c39f8a7 100644 --- a/Mathlib/RingTheory/Lasker.lean +++ b/Mathlib/RingTheory/Lasker.lean @@ -57,6 +57,7 @@ lemma decomposition_erase_inf [DecidableEq (Ideal R)] {I : Ideal R} open scoped Function -- required for scoped `on` notation +set_option trace.profiler true in lemma isPrimary_decomposition_pairwise_ne_radical {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) : ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧ @@ -64,16 +65,8 @@ lemma isPrimary_decomposition_pairwise_ne_radical {I : Ideal R} classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ - · rw [← hs] - refine le_antisymm ?_ ?_ <;> intro x hx - · simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, - Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ - intro J hJ - exact hx J hJ J hJ rfl - · simp only [Submodule.mem_finsetInf, id_eq, Finset.inf_image, CompTriple.comp_eq, - Function.comp_apply, Finset.mem_filter, and_imp] at hx ⊢ - intro J _ K hK _ - exact hx K hK + · ext + grind [Finset.inf_image, Submodule.mem_finsetInf] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ ``` ``` ℹ [1261/1261] Built Mathlib.RingTheory.Lasker (1.2s) info: Mathlib/RingTheory/Lasker.lean:61:0: [Elab.command] [0.011121] theorem isPrimary_decomposition_pairwise_ne_radical {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) : ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧ (t : Set (Ideal R)).Pairwise ((· ≠ ·) on radical) := by classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · ext grind [Finset.inf_image, Submodule.mem_finsetInf] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] info: Mathlib/RingTheory/Lasker.lean:61:0: [Elab.command] [0.012898] lemma isPrimary_decomposition_pairwise_ne_radical {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) : ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧ (t : Set (Ideal R)).Pairwise ((· ≠ ·) on radical) := by classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · ext grind [Finset.inf_image, Submodule.mem_finsetInf] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] info: Mathlib/RingTheory/Lasker.lean:61:0: [Elab.async] [0.157957] elaborating proof of Ideal.isPrimary_decomposition_pairwise_ne_radical [Elab.definition.value] [0.156050] Ideal.isPrimary_decomposition_pairwise_ne_radical [Elab.step] [0.154194] classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · ext grind [Finset.inf_image, Submodule.mem_finsetInf] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.154189] classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · ext grind [Finset.inf_image, Submodule.mem_finsetInf] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.154184] classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · ext grind [Finset.inf_image, Submodule.mem_finsetInf] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, [… 59 lines omitted …] ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ [Elab.step] [0.017062] expected type: ∃ t, t.inf id = I ∧ (∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary) ∧ (↑t).Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on radical), term ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ [Elab.step] [0.017043] expected type: ∃ t, t.inf id = I ∧ (∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary) ∧ (↑t).Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on radical), term Exists.intro✝ ((s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id) ⟨?_, ?_, ?_⟩ [Elab.step] [0.016253] expected type: Finset (Ideal R), term (s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id [Elab.step] [0.013756] expected type: , term (s.image (fun J ↦ {I ∈ s | I.radical = J.radical})) [Elab.step] [0.013751] expected type: , term s.image (fun J ↦ {I ∈ s | I.radical = J.radical}) [Elab.step] [0.011627] expected type: ?m.44 → Finset (Ideal R), term (fun J ↦ {I ∈ s | I.radical = J.radical}) [Elab.step] [0.011622] expected type: ?m.44 → Finset (Ideal R), term fun J ↦ {I ∈ s | I.radical = J.radical} [Elab.step] [0.011555] expected type: Finset (Ideal R), term {I ∈ s | I.radical = J.radical} [Elab.step] [0.090158] · ext grind [Finset.inf_image, Submodule.mem_finsetInf] [Elab.step] [0.090093] ext grind [Finset.inf_image, Submodule.mem_finsetInf] [Elab.step] [0.090089] ext grind [Finset.inf_image, Submodule.mem_finsetInf] [Elab.step] [0.089120] grind [Finset.inf_image, Submodule.mem_finsetInf] [Elab.step] [0.014619] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] [Elab.step] [0.014610] simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] [Elab.step] [0.014605] simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] [Elab.step] [0.026753] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.026740] intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.026737] intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.013805] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.013799] rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.013796] rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] Build completed successfully (1261 jobs). ```
--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) 		t-ring-theory maintainer-merge 2/10 Mathlib/RingTheory/Lasker.lean 1 2 ['erdOne', 'github-actions'] nobody
5-72314
5 days ago
5-72314
5 days ago
11-44489
11 days
31055 jsm28
author:jsm28
 feat(Geometry/Euclidean/Projection): `orthogonalProjectionSpan_congr` Add a congruence lemma for `orthogonalProjectionSpan` applied to two simplices with the same set of vertices, analogous to and proved using `orthogonalProjection_congr`, and a variant `orthogonalProjectionSpan_reindex`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-euclidean-geometry 10/0 Mathlib/Geometry/Euclidean/Projection.lean 1 3 ['JovanGerb', 'github-actions'] JovanGerb
assignee:JovanGerb
4-65551
4 days ago
4-65551
4 days ago
15-73340
15 days
30348 RemyDegenne
author:RemyDegenne
 feat: convergence in probability implies convergence in distribution Prove that convergence in probability implies convergence in distribution, as well as Slutsky's theorem on the convergence of a product of random variables (since those two facts follow from the same lemma). --- - [x] depends on: #30346 - [x] depends on: #30385 - [x] depends on: #30402 - [x] depends on: #30540 - [x] depends on: #30585 - [x] depends on: #30742 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-measure-probability 256/2 Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean,Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean,Mathlib/Topology/EMetricSpace/Lipschitz.lean,Mathlib/Topology/Instances/ENNReal/Lemmas.lean,docs/1000.yaml 5 21 ['EtienneC30', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] EtienneC30
assignee:EtienneC30
3-78336
3 days ago
5-44043
5 days ago
13-12648
13 days
31506 FLDutchmann
author:FLDutchmann
 feat: Qq version of getLevel These were helpful for writing the `algebra` tactic for adding Qq annotations in cases where I know that an expression is a type. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta 11/2 Mathlib/Util/Qq.lean 1 6 ['FLDutchmann', 'github-actions', 'grunweg'] nobody
2-58143
2 days ago
2-58143
2 days ago
2-65484
2 days
31227 YaelDillies
author:YaelDillies
 feat(Algebra/Homology): sandwich a comm group between two finite comm groups From ClassFieldTheory --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) CFT maintainer-merge t-algebra
label:t-algebra$
 64/39 Mathlib/Algebra/Homology/ShortComplex/Ab.lean,Mathlib/Data/Finite/Prod.lean,Mathlib/Data/Set/Finite/Basic.lean,Mathlib/GroupTheory/QuotientGroup/Finite.lean,Mathlib/RingTheory/Ideal/Quotient/Basic.lean,Mathlib/Topology/Algebra/Valued/LocallyCompact.lean 6 10 ['YaelDillies', 'erdOne', 'github-actions', 'jcommelin'] erdOne
assignee:erdOne
2-53656
2 days ago
2-72857
2 days ago
10-49338
10 days
31250 joelriou
author:joelriou
 feat(AlgebraicTopology): inductive construction of StrictSegal structures We obtain a computable `StrictSegal (nerve C)` structure by using an inductive construction based on a new `StrictSegalCore` structure which provides a way to construct a `n + 1`-simplex by from a `1`-simplex and a `n`-simplex satisfying a compatibility. --- - [x] depends on: #31248 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 177/29 Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean,Mathlib/AlgebraicTopology/SimplicialSet/Path.lean,Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean,Mathlib/CategoryTheory/ComposableArrows.lean 4 20 ['emilyriehl', 'github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'robin-carlier'] dagurtomas
assignee:dagurtomas
2-26075
2 days ago
9-56653
9 days ago
9-66953
9 days
31537 RemyDegenne
author:RemyDegenne
 feat: totally bounded sets have finite covers New result: a totally bounded set has finite `ε`-covers for all `ε > 0`. I then use it to golf and generalize `exists_finite_isCover_of_isCompact_closure` and `exists_finite_isCover_of_isCompact` to extended pseudo-metric spaces. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 36/17 Mathlib/Data/Rel/Cover.lean,Mathlib/Topology/MetricSpace/Cover.lean 2 7 ['YaelDillies', 'github-actions'] nobody
1-76242
1 day ago
1-76242
1 day ago
1-77947
1 day
31540 themathqueen
author:themathqueen
 chore: move `LinearAlgebra/Matrix/HermitianFunctionalCalculus` to `Analysis/Matrix` `Analysis/Matrix` is a more appropriate location for this as these are analysis results and depends on `Analysis/Matrix/Spectrum`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed maintainer-merge t-analysis 2/2 Mathlib.lean,Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean,Mathlib/Analysis/Matrix/Order.lean 3 6 ['Vierkantor', 'github-actions', 'grunweg'] nobody
1-70270
1 day ago
1-76344
1 day ago
1-77849
1 day
30201 luigi-massacci
author:luigi-massacci
 feat: add differentiation for ContDiffMapSupportedIn Add a wrapper for `iteratedFDeriv` on `ContDiffMapSupportedIn` and related API. --- - [x] depends on: #30199 - [x] depends on: #30198 - [x] depends on: #30197 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-analysis 180/11 Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean,Mathlib/Topology/ContinuousMap/Bounded/Basic.lean 2 44 ['ADedecker', 'github-actions', 'grunweg', 'luigi-massacci', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] nobody
1-57992
1 day ago
1-63819
1 day ago
5-54709
5 days
31497 staroperator
author:staroperator
 feat(Algebra/Group): semigroup ideals This PR defines semigroup ideals; they are different from (in fact, a weaker form of) ring ideals. We prove that in a monoid whose algebraic order is well-quasi-order, all semigroup ideals are finitely generated, and the semigroup ideals satisfy the ascending chain condition. These definitions and results are useful in #27414. Note: Following `Ideal` with `Submodule`, `SemigroupIdeal M` is an `abbrev` of `SubMulAction M M`. Also, `Ideal.closure` is a re-definition of `SubMulAction.closure` and `Ideal.FG` is defeq to `SubMulAction.FG` but unfolds more nicely. --- - [x] depends on: #31517 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
 194/0 Mathlib.lean,Mathlib/Algebra/Group/Ideal.lean,Mathlib/Algebra/Order/Group/Ideal.lean 3 24 ['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'staroperator'] nobody
1-43368
1 day ago
1-57823
1 day ago
2-78684
2 days
31273 euprunin
author:euprunin
 chore(MeasureTheory/MeasurableSpace): golf `measurableSet_generateFrom_singleton_iff` using `grind` ---
Show trace profiling of measurableSet_generateFrom_singleton_iff: 70 ms before, 91 ms after ### Trace profiling of `measurableSet_generateFrom_singleton_iff` before PR 31273 ```diff diff --git a/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean b/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean index baf5299a16..fb8e3fc16d 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean @@ -42,6 +42,7 @@ end MeasurableSpace namespace MeasureTheory +set_option trace.profiler true in theorem measurableSet_generateFrom_singleton_iff {s t : Set α} : MeasurableSet[MeasurableSpace.generateFrom {s}] t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ := by simp_rw [MeasurableSpace.generateFrom_singleton] ``` ``` ℹ [880/880] Built Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (1.2s) info: Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean:46:0: [Elab.async] [0.071352] elaborating proof of MeasureTheory.measurableSet_generateFrom_singleton_iff [Elab.definition.value] [0.069878] MeasureTheory.measurableSet_generateFrom_singleton_iff [Elab.step] [0.068734] simp_rw [MeasurableSpace.generateFrom_singleton] unfold MeasurableSet MeasurableSpace.MeasurableSet' MeasurableSpace.comap simp_rw [MeasurableSpace.measurableSet_top, true_and] constructor · rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · refine Or.inr <| Or.inr <| Or.inr <| subset_antisymm (subset_univ _) ?_ suffices x = univ by simp only [this, preimage_univ, subset_refl] refine subset_antisymm (subset_univ _) ?_ rw [univ_eq_true_false] rintro - (rfl | rfl) · assumption · assumption · have hx : x = { True } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ by_contra hpneg rw [eq_iff_iff, iff_true, ← false_iff] at hpneg exact hF (by convert hp) simp [hx] · by_cases hF : False ∈ x · have hx : x = { False } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hF⟩ grind refine Or.inr <| Or.inr <| Or.inl <| ?_ simp [hx, compl_def] · refine Or.inl <| subset_antisymm ?_ <| empty_subset _ suffices x ⊆ ∅ by rw [subset_empty_iff] at this simp only [this, preimage_empty, subset_refl] intro p hp fin_cases p · contradiction · contradiction · rintro (rfl | rfl | rfl | rfl) on_goal 1 => use ∅ on_goal 2 => use { True } on_goal 3 => use { False } on_goal 4 => use Set.univ all_goals simp [compl_def] [Elab.step] [0.068727] simp_rw [MeasurableSpace.generateFrom_singleton] unfold MeasurableSet MeasurableSpace.MeasurableSet' MeasurableSpace.comap simp_rw [MeasurableSpace.measurableSet_top, true_and] constructor · rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · refine Or.inr <| Or.inr <| Or.inr <| subset_antisymm (subset_univ _) ?_ suffices x = univ by simp only [this, preimage_univ, subset_refl] refine subset_antisymm (subset_univ _) ?_ rw [univ_eq_true_false] rintro - (rfl | rfl) · assumption · assumption · have hx : x = { True } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ by_contra hpneg rw [eq_iff_iff, iff_true, ← false_iff] at hpneg exact hF (by convert hp) simp [hx] · by_cases hF : False ∈ x · have hx : x = { False } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hF⟩ grind refine Or.inr <| Or.inr <| Or.inl <| ?_ simp [hx, compl_def] · refine Or.inl <| subset_antisymm ?_ <| empty_subset _ suffices x ⊆ ∅ by rw [subset_empty_iff] at this simp only [this, preimage_empty, subset_refl] intro p hp fin_cases p · contradiction · contradiction · rintro (rfl | rfl | rfl | rfl) on_goal 1 => use ∅ on_goal 2 => use { True } on_goal 3 => use { False } on_goal 4 => use Set.univ all_goals simp [compl_def] [Elab.step] [0.012541] simp_rw [MeasurableSpace.generateFrom_singleton] [Elab.step] [0.041180] · rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · refine Or.inr <| Or.inr <| Or.inr <| subset_antisymm (subset_univ _) ?_ suffices x = univ by simp only [this, preimage_univ, subset_refl] refine subset_antisymm (subset_univ _) ?_ rw [univ_eq_true_false] rintro - (rfl | rfl) · assumption [… 112 lines omitted …] · assumption · assumption · have hx : x = { True } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ by_contra hpneg rw [eq_iff_iff, iff_true, ← false_iff] at hpneg exact hF (by convert hp) simp [hx] [Elab.step] [0.028797] by_cases hF : False ∈ x · refine Or.inr <| Or.inr <| Or.inr <| subset_antisymm (subset_univ _) ?_ suffices x = univ by simp only [this, preimage_univ, subset_refl] refine subset_antisymm (subset_univ _) ?_ rw [univ_eq_true_false] rintro - (rfl | rfl) · assumption · assumption · have hx : x = { True } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ by_contra hpneg rw [eq_iff_iff, iff_true, ← false_iff] at hpneg exact hF (by convert hp) simp [hx] [Elab.step] [0.025079] · have hx : x = { True } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ by_contra hpneg rw [eq_iff_iff, iff_true, ← false_iff] at hpneg exact hF (by convert hp) simp [hx] [Elab.step] [0.025059] have hx : x = { True } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ by_contra hpneg rw [eq_iff_iff, iff_true, ← false_iff] at hpneg exact hF (by convert hp) simp [hx] [Elab.step] [0.025057] have hx : x = { True } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ by_contra hpneg rw [eq_iff_iff, iff_true, ← false_iff] at hpneg exact hF (by convert hp) simp [hx] [Elab.step] [0.015096] simp [hx] [Meta.synthInstance] [0.011997] ❌️ Nontrivial (Set α) [Elab.step] [0.011467] · by_cases hF : False ∈ x · have hx : x = { False } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hF⟩ grind refine Or.inr <| Or.inr <| Or.inl <| ?_ simp [hx, compl_def] · refine Or.inl <| subset_antisymm ?_ <| empty_subset _ suffices x ⊆ ∅ by rw [subset_empty_iff] at this simp only [this, preimage_empty, subset_refl] intro p hp fin_cases p · contradiction · contradiction [Elab.step] [0.011367] by_cases hF : False ∈ x · have hx : x = { False } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hF⟩ grind refine Or.inr <| Or.inr <| Or.inl <| ?_ simp [hx, compl_def] · refine Or.inl <| subset_antisymm ?_ <| empty_subset _ suffices x ⊆ ∅ by rw [subset_empty_iff] at this simp only [this, preimage_empty, subset_refl] intro p hp fin_cases p · contradiction · contradiction [Elab.step] [0.011363] by_cases hF : False ∈ x · have hx : x = { False } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hF⟩ grind refine Or.inr <| Or.inr <| Or.inl <| ?_ simp [hx, compl_def] · refine Or.inl <| subset_antisymm ?_ <| empty_subset _ suffices x ⊆ ∅ by rw [subset_empty_iff] at this simp only [this, preimage_empty, subset_refl] intro p hp fin_cases p · contradiction · contradiction Build completed successfully (880 jobs). ``` ### Trace profiling of `measurableSet_generateFrom_singleton_iff` after PR 31273 ```diff diff --git a/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean b/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean index baf5299a16..b67f37d372 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean @@ -42,6 +42,7 @@ end MeasurableSpace namespace MeasureTheory +set_option trace.profiler true in theorem measurableSet_generateFrom_singleton_iff {s t : Set α} : MeasurableSet[MeasurableSpace.generateFrom {s}] t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ := by simp_rw [MeasurableSpace.generateFrom_singleton] @@ -51,35 +52,14 @@ theorem measurableSet_generateFrom_singleton_iff {s t : Set α} : · rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x - · refine Or.inr <| Or.inr <| Or.inr <| subset_antisymm (subset_univ _) ?_ - suffices x = univ by simp only [this, preimage_univ, subset_refl] - refine subset_antisymm (subset_univ _) ?_ - rw [univ_eq_true_false] - rintro - (rfl | rfl) - · assumption - · assumption - · have hx : x = {True} := by - ext p - refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ - by_contra hpneg - rw [eq_iff_iff, iff_true, ← false_iff] at hpneg - exact hF (by convert hp) - simp [hx] + · suffices x = univ by grind + grind [univ_eq_true_false] + · grind · by_cases hF : False ∈ x - · have hx : x = {False} := by - ext p - refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hF⟩ - grind - refine Or.inr <| Or.inr <| Or.inl <| ?_ - simp [hx, compl_def] - · refine Or.inl <| subset_antisymm ?_ <| empty_subset _ - suffices x ⊆ ∅ by - rw [subset_empty_iff] at this - simp only [this, preimage_empty, subset_refl] + · grind + · suffices x ⊆ ∅ by grind intro p hp - fin_cases p - · contradiction - · contradiction + fin_cases p <;> contradiction · rintro (rfl | rfl | rfl | rfl) on_goal 1 => use ∅ on_goal 2 => use {True} ``` ``` ℹ [880/880] Built Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (1.2s) info: Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean:46:0: [Elab.async] [0.092756] elaborating proof of MeasureTheory.measurableSet_generateFrom_singleton_iff [Elab.definition.value] [0.091377] MeasureTheory.measurableSet_generateFrom_singleton_iff [Elab.step] [0.090497] simp_rw [MeasurableSpace.generateFrom_singleton] unfold MeasurableSet MeasurableSpace.MeasurableSet' MeasurableSpace.comap simp_rw [MeasurableSpace.measurableSet_top, true_and] constructor · rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind · by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction · rintro (rfl | rfl | rfl | rfl) on_goal 1 => use ∅ on_goal 2 => use { True } on_goal 3 => use { False } on_goal 4 => use Set.univ all_goals simp [compl_def] [Elab.step] [0.090489] simp_rw [MeasurableSpace.generateFrom_singleton] unfold MeasurableSet MeasurableSpace.MeasurableSet' MeasurableSpace.comap simp_rw [MeasurableSpace.measurableSet_top, true_and] constructor · rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind · by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction · rintro (rfl | rfl | rfl | rfl) on_goal 1 => use ∅ on_goal 2 => use { True } on_goal 3 => use { False } on_goal 4 => use Set.univ all_goals simp [compl_def] [Elab.step] [0.012749] simp_rw [MeasurableSpace.generateFrom_singleton] [Elab.step] [0.062153] · rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind · by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.062134] rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind · by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.062131] rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind · by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.031421] · by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind [Elab.step] [0.031410] by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind [Elab.step] [0.031407] by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind [Elab.step] [0.019456] · suffices x = univ by grind grind [univ_eq_true_false] [Elab.step] [0.019448] suffices x = univ by grind grind [univ_eq_true_false] [Elab.step] [0.019444] suffices x = univ by grind grind [univ_eq_true_false] [Elab.step] [0.010344] grind [univ_eq_true_false] [Elab.step] [0.011419] · grind [Elab.step] [0.011411] grind [Elab.step] [0.011407] grind [Elab.step] [0.011402] grind [Elab.step] [0.029820] · by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.029812] by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.029808] by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.011217] · grind [Elab.step] [0.011211] grind [Elab.step] [0.011208] grind [Elab.step] [0.011203] grind [Elab.step] [0.017927] · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.017920] suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.017914] suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.014460] suffices x ⊆ ∅ by grind [Elab.step] [0.014455] refine_lift suffices x ⊆ ∅ by grind; ?_ [Elab.step] [0.014451] focus (refine no_implicit_lambda% (suffices x ⊆ ∅ by grind; ?_); rotate_right) [Elab.step] [0.014447] (refine no_implicit_lambda% (suffices x ⊆ ∅ by grind; ?_); rotate_right) [Elab.step] [0.014445] (refine no_implicit_lambda% (suffices x ⊆ ∅ by grind; ?_); rotate_right) [Elab.step] [0.014442] (refine no_implicit_lambda% (suffices x ⊆ ∅ by grind; ?_); rotate_right) [Elab.step] [0.014440] refine no_implicit_lambda% (suffices x ⊆ ∅ by grind; ?_); rotate_right [Elab.step] [0.014438] refine no_implicit_lambda% (suffices x ⊆ ∅ by grind; ?_); rotate_right [Elab.step] [0.014428] refine no_implicit_lambda% (suffices x ⊆ ∅ by grind; ?_) [Elab.step] [0.013889] grind [Elab.step] [0.013885] grind [Elab.step] [0.013879] grind Build completed successfully (880 jobs). ```
--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) 		maintainer-merge t-measure-probability 6/27 Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean 1 3 ['EtienneC30', 'github-actions'] EtienneC30
assignee:EtienneC30
1-41936
1 day ago
1-41936
1 day ago
8-83381
8 days
31398 YaelDillies
author:YaelDillies
 feat(MeasureTheory/Measure): `comap_apply` version for measurable equivs This one is stated in terms of the preimage of the inverse, which is sometimes (but not always!) more useful than the image of the forward map. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-measure-probability 13/0 Mathlib/MeasureTheory/Measure/Restrict.lean 1 4 ['EtienneC30', 'YaelDillies', 'github-actions'] EtienneC30
assignee:EtienneC30
1-40781
1 day ago
1-40806
1 day ago
5-33993
5 days
31278 ADedecker
author:ADedecker
 feat: approximate continuous functions by smooth functions This is motivated by #31079, and adapted from [this lemma](https://github.com/leanprover-community/sphere-eversion/blob/master/SphereEversion/ToMathlib/ExistsOfConvex.lean#L213) in the Sphere Eversion project. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-analysis t-differential-geometry 157/0 Mathlib.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/FDeriv/Const.lean,Mathlib/Analysis/Convex/Basic.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean,Mathlib/Geometry/Manifold/SmoothApprox.lean 7 36 ['ADedecker', 'github-actions', 'grunweg', 'mcdoll', 'sgouezel'] grunweg
assignee:grunweg
1-35442
1 day ago
7-60030
7 days ago
8-48995
8 days
30650 JovanGerb
author:JovanGerb
 perf(reassoc, to_app, elementwise): don't pass the same proof to the kernel again In `reassoc`, `to_app`, `elementwise`, the proof of the original lemma was being used to prove the modified lemma. This is silly, because the modified lemma can be proved using the original lemma directly. Hence, this PR modifies `addRelatedDecl` to include this optimization. Previously, `addRelatedDecl` would pass around both the type and the value of the original declaration. This was necessary, because the inferred type of the value might not be identical to the type it is given. Now this is not necessary anymore, because the type of the constant is exactly the type that it is given, so the type can always be obtained with `inferType`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta 19/21 Mathlib/Tactic/CategoryTheory/Elementwise.lean,Mathlib/Tactic/CategoryTheory/Reassoc.lean,Mathlib/Tactic/CategoryTheory/ToApp.lean,Mathlib/Util/AddRelatedDecl.lean 4 13 ['JovanGerb', 'dwrensha', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'plp127'] dwrensha
assignee:dwrensha
1-27737
1 day ago
1-69253
1 day ago
26-58555
26 days
31535 ADedecker
author:ADedecker
 feat: small tweaks to `PointwiseConvergenceCLM` These are small suggestions I would have made about #11496: - add a `IsUniformEmbedding` variant of `isEmbedding_coeFn` - add a `ContinuousEvalConst` instance using [UniformConvergenceCLM.continuousEvalConst](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/Module/StrongTopology.html#UniformConvergenceCLM.continuousEvalConst) - use said instance to golf continuity in `evalCLM` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 16/11 Mathlib/Topology/Algebra/Module/PointwiseConvergence.lean 1 3 ['github-actions', 'mcdoll'] nobody
1-25338
1 day ago
1-25338
1 day ago
1-80598
1 day

All maintainer merge'd PRs

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
30047 ooovi
author:ooovi
 feat(Combinatorics/SimpleGraph): edge labellings Add edge labellings for `SimpleGraph` as well as some basic lemmata. --- This is mostly a cleaned up part of @b-mehta's lean4 port of their [formalisation of an exponentially better upper bound on Ramsey numbers ](https://github.com/b-mehta/ExponentialRamsey/). I need these definitions for another project on Ramsey theory. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-combinatorics awaiting-author 234/3 Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/EdgeLabelling.lean,Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean,Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean 5 52 ['YaelDillies', 'b-mehta', 'github-actions', 'ooovi', 'vlad902'] b-mehta
assignee:b-mehta
6-8643
6 days ago
10-1364
10 days ago
34-69915
34 days
31201 euprunin
author:euprunin
 chore(RingTheory): golf `isPrimary_decomposition_pairwise_ne_radical` using `grind` ---
Show trace profiling of isPrimary_decomposition_pairwise_ne_radical: 89 ms before, 156 ms after ### Trace profiling of `isPrimary_decomposition_pairwise_ne_radical` before PR 31201 ```diff diff --git a/Mathlib/RingTheory/Lasker.lean b/Mathlib/RingTheory/Lasker.lean index 8f522d48f8..21bf4d68b6 100644 --- a/Mathlib/RingTheory/Lasker.lean +++ b/Mathlib/RingTheory/Lasker.lean @@ -57,6 +57,7 @@ lemma decomposition_erase_inf [DecidableEq (Ideal R)] {I : Ideal R} open scoped Function -- required for scoped `on` notation +set_option trace.profiler true in lemma isPrimary_decomposition_pairwise_ne_radical {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) : ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧ ``` ``` ℹ [1261/1261] Built Mathlib.RingTheory.Lasker (1.3s) info: Mathlib/RingTheory/Lasker.lean:61:0: [Elab.command] [0.013044] theorem isPrimary_decomposition_pairwise_ne_radical {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) : ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧ (t : Set (Ideal R)).Pairwise ((· ≠ ·) on radical) := by classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · rw [← hs] refine le_antisymm ?_ ?_ <;> intro x hx · simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl · simp only [Submodule.mem_finsetInf, id_eq, Finset.inf_image, CompTriple.comp_eq, Function.comp_apply, Finset.mem_filter, and_imp] at hx ⊢ intro J _ K hK _ exact hx K hK · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.definition.header] [0.010071] Ideal.isPrimary_decomposition_pairwise_ne_radical info: Mathlib/RingTheory/Lasker.lean:61:0: [Elab.command] [0.016459] lemma isPrimary_decomposition_pairwise_ne_radical {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) : ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧ (t : Set (Ideal R)).Pairwise ((· ≠ ·) on radical) := by classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · rw [← hs] refine le_antisymm ?_ ?_ <;> intro x hx · simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl · simp only [Submodule.mem_finsetInf, id_eq, Finset.inf_image, CompTriple.comp_eq, Function.comp_apply, Finset.mem_filter, and_imp] at hx ⊢ intro J _ K hK _ exact hx K hK · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] info: Mathlib/RingTheory/Lasker.lean:61:0: [Elab.async] [0.091697] elaborating proof of Ideal.isPrimary_decomposition_pairwise_ne_radical [Elab.definition.value] [0.089099] Ideal.isPrimary_decomposition_pairwise_ne_radical [Elab.step] [0.086924] classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · rw [← hs] refine le_antisymm ?_ ?_ <;> intro x hx · simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl · simp only [Submodule.mem_finsetInf, id_eq, Finset.inf_image, CompTriple.comp_eq, Function.comp_apply, Finset.mem_filter, and_imp] at hx ⊢ intro J _ K hK _ exact hx K hK · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.086918] classical [… 154 lines omitted …] Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl · simp only [Submodule.mem_finsetInf, id_eq, Finset.inf_image, CompTriple.comp_eq, Function.comp_apply, Finset.mem_filter, and_imp] at hx ⊢ intro J _ K hK _ exact hx K hK [Elab.step] [0.020717] rw [← hs] refine le_antisymm ?_ ?_ <;> intro x hx · simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl · simp only [Submodule.mem_finsetInf, id_eq, Finset.inf_image, CompTriple.comp_eq, Function.comp_apply, Finset.mem_filter, and_imp] at hx ⊢ intro J _ K hK _ exact hx K hK [Elab.step] [0.010102] · simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl [Elab.step] [0.010064] simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl [Elab.step] [0.010060] simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ intro J hJ exact hx J hJ J hJ rfl [Elab.step] [0.015365] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] [Elab.step] [0.015273] simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] [Elab.step] [0.015268] simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] [Elab.step] [0.027960] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.027947] intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.027944] intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.014324] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.014317] rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.014310] rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] Build completed successfully (1261 jobs). ``` ### Trace profiling of `isPrimary_decomposition_pairwise_ne_radical` after PR 31201 ```diff diff --git a/Mathlib/RingTheory/Lasker.lean b/Mathlib/RingTheory/Lasker.lean index 8f522d48f8..6f1c39f8a7 100644 --- a/Mathlib/RingTheory/Lasker.lean +++ b/Mathlib/RingTheory/Lasker.lean @@ -57,6 +57,7 @@ lemma decomposition_erase_inf [DecidableEq (Ideal R)] {I : Ideal R} open scoped Function -- required for scoped `on` notation +set_option trace.profiler true in lemma isPrimary_decomposition_pairwise_ne_radical {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) : ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧ @@ -64,16 +65,8 @@ lemma isPrimary_decomposition_pairwise_ne_radical {I : Ideal R} classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ - · rw [← hs] - refine le_antisymm ?_ ?_ <;> intro x hx - · simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finsetInf, - Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢ - intro J hJ - exact hx J hJ J hJ rfl - · simp only [Submodule.mem_finsetInf, id_eq, Finset.inf_image, CompTriple.comp_eq, - Function.comp_apply, Finset.mem_filter, and_imp] at hx ⊢ - intro J _ K hK _ - exact hx K hK + · ext + grind [Finset.inf_image, Submodule.mem_finsetInf] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ ``` ``` ℹ [1261/1261] Built Mathlib.RingTheory.Lasker (1.2s) info: Mathlib/RingTheory/Lasker.lean:61:0: [Elab.command] [0.011121] theorem isPrimary_decomposition_pairwise_ne_radical {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) : ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧ (t : Set (Ideal R)).Pairwise ((· ≠ ·) on radical) := by classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · ext grind [Finset.inf_image, Submodule.mem_finsetInf] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] info: Mathlib/RingTheory/Lasker.lean:61:0: [Elab.command] [0.012898] lemma isPrimary_decomposition_pairwise_ne_radical {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) : ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧ (t : Set (Ideal R)).Pairwise ((· ≠ ·) on radical) := by classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · ext grind [Finset.inf_image, Submodule.mem_finsetInf] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] info: Mathlib/RingTheory/Lasker.lean:61:0: [Elab.async] [0.157957] elaborating proof of Ideal.isPrimary_decomposition_pairwise_ne_radical [Elab.definition.value] [0.156050] Ideal.isPrimary_decomposition_pairwise_ne_radical [Elab.step] [0.154194] classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · ext grind [Finset.inf_image, Submodule.mem_finsetInf] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.154189] classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · ext grind [Finset.inf_image, Submodule.mem_finsetInf] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.154184] classical refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ · ext grind [Finset.inf_image, Submodule.mem_finsetInf] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, [… 59 lines omitted …] ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ [Elab.step] [0.017062] expected type: ∃ t, t.inf id = I ∧ (∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary) ∧ (↑t).Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on radical), term ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id, ?_, ?_, ?_⟩ [Elab.step] [0.017043] expected type: ∃ t, t.inf id = I ∧ (∀ ⦃J : Ideal R⦄, J ∈ t → J.IsPrimary) ∧ (↑t).Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on radical), term Exists.intro✝ ((s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id) ⟨?_, ?_, ?_⟩ [Elab.step] [0.016253] expected type: Finset (Ideal R), term (s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id [Elab.step] [0.013756] expected type: , term (s.image (fun J ↦ {I ∈ s | I.radical = J.radical})) [Elab.step] [0.013751] expected type: , term s.image (fun J ↦ {I ∈ s | I.radical = J.radical}) [Elab.step] [0.011627] expected type: ?m.44 → Finset (Ideal R), term (fun J ↦ {I ∈ s | I.radical = J.radical}) [Elab.step] [0.011622] expected type: ?m.44 → Finset (Ideal R), term fun J ↦ {I ∈ s | I.radical = J.radical} [Elab.step] [0.011555] expected type: Finset (Ideal R), term {I ∈ s | I.radical = J.radical} [Elab.step] [0.090158] · ext grind [Finset.inf_image, Submodule.mem_finsetInf] [Elab.step] [0.090093] ext grind [Finset.inf_image, Submodule.mem_finsetInf] [Elab.step] [0.090089] ext grind [Finset.inf_image, Submodule.mem_finsetInf] [Elab.step] [0.089120] grind [Finset.inf_image, Submodule.mem_finsetInf] [Elab.step] [0.014619] · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] [Elab.step] [0.014610] simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] [Elab.step] [0.014605] simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro J hJ refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp) · simp [hJ] · simp only [Finset.mem_filter, id_eq, and_imp] intro y hy simp [hs' hy] [Elab.step] [0.026753] · intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.026740] intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.026737] intro I hI J hJ hIJ simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] contrapose! hIJ suffices I'.radical = J'.radical by rw [← hI, ← hJ, this] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.013805] · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.013799] rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] [Elab.step] [0.013796] rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq] Build completed successfully (1261 jobs). ```
--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) 		t-ring-theory maintainer-merge 2/10 Mathlib/RingTheory/Lasker.lean 1 2 ['erdOne', 'github-actions'] nobody
5-72314
5 days ago
5-72314
5 days ago
11-44489
11 days
31055 jsm28
author:jsm28
 feat(Geometry/Euclidean/Projection): `orthogonalProjectionSpan_congr` Add a congruence lemma for `orthogonalProjectionSpan` applied to two simplices with the same set of vertices, analogous to and proved using `orthogonalProjection_congr`, and a variant `orthogonalProjectionSpan_reindex`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-euclidean-geometry 10/0 Mathlib/Geometry/Euclidean/Projection.lean 1 3 ['JovanGerb', 'github-actions'] JovanGerb
assignee:JovanGerb
4-65551
4 days ago
4-65551
4 days ago
15-73340
15 days
30348 RemyDegenne
author:RemyDegenne
 feat: convergence in probability implies convergence in distribution Prove that convergence in probability implies convergence in distribution, as well as Slutsky's theorem on the convergence of a product of random variables (since those two facts follow from the same lemma). --- - [x] depends on: #30346 - [x] depends on: #30385 - [x] depends on: #30402 - [x] depends on: #30540 - [x] depends on: #30585 - [x] depends on: #30742 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-measure-probability 256/2 Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean,Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean,Mathlib/Topology/EMetricSpace/Lipschitz.lean,Mathlib/Topology/Instances/ENNReal/Lemmas.lean,docs/1000.yaml 5 21 ['EtienneC30', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] EtienneC30
assignee:EtienneC30
3-78336
3 days ago
5-44043
5 days ago
13-12648
13 days
31506 FLDutchmann
author:FLDutchmann
 feat: Qq version of getLevel These were helpful for writing the `algebra` tactic for adding Qq annotations in cases where I know that an expression is a type. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta 11/2 Mathlib/Util/Qq.lean 1 6 ['FLDutchmann', 'github-actions', 'grunweg'] nobody
2-58143
2 days ago
2-58143
2 days ago
2-65484
2 days
31227 YaelDillies
author:YaelDillies
 feat(Algebra/Homology): sandwich a comm group between two finite comm groups From ClassFieldTheory --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) CFT maintainer-merge t-algebra
label:t-algebra$
 64/39 Mathlib/Algebra/Homology/ShortComplex/Ab.lean,Mathlib/Data/Finite/Prod.lean,Mathlib/Data/Set/Finite/Basic.lean,Mathlib/GroupTheory/QuotientGroup/Finite.lean,Mathlib/RingTheory/Ideal/Quotient/Basic.lean,Mathlib/Topology/Algebra/Valued/LocallyCompact.lean 6 10 ['YaelDillies', 'erdOne', 'github-actions', 'jcommelin'] erdOne
assignee:erdOne
2-53656
2 days ago
2-72857
2 days ago
10-49338
10 days
31250 joelriou
author:joelriou
 feat(AlgebraicTopology): inductive construction of StrictSegal structures We obtain a computable `StrictSegal (nerve C)` structure by using an inductive construction based on a new `StrictSegalCore` structure which provides a way to construct a `n + 1`-simplex by from a `1`-simplex and a `n`-simplex satisfying a compatibility. --- - [x] depends on: #31248 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 177/29 Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean,Mathlib/AlgebraicTopology/SimplicialSet/Path.lean,Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean,Mathlib/CategoryTheory/ComposableArrows.lean 4 20 ['emilyriehl', 'github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'robin-carlier'] dagurtomas
assignee:dagurtomas
2-26075
2 days ago
9-56653
9 days ago
9-66953
9 days
31537 RemyDegenne
author:RemyDegenne
 feat: totally bounded sets have finite covers New result: a totally bounded set has finite `ε`-covers for all `ε > 0`. I then use it to golf and generalize `exists_finite_isCover_of_isCompact_closure` and `exists_finite_isCover_of_isCompact` to extended pseudo-metric spaces. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 36/17 Mathlib/Data/Rel/Cover.lean,Mathlib/Topology/MetricSpace/Cover.lean 2 7 ['YaelDillies', 'github-actions'] nobody
1-76242
1 day ago
1-76242
1 day ago
1-77947
1 day
31540 themathqueen
author:themathqueen
 chore: move `LinearAlgebra/Matrix/HermitianFunctionalCalculus` to `Analysis/Matrix` `Analysis/Matrix` is a more appropriate location for this as these are analysis results and depends on `Analysis/Matrix/Spectrum`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed maintainer-merge t-analysis 2/2 Mathlib.lean,Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean,Mathlib/Analysis/Matrix/Order.lean 3 6 ['Vierkantor', 'github-actions', 'grunweg'] nobody
1-70270
1 day ago
1-76344
1 day ago
1-77849
1 day
30201 luigi-massacci
author:luigi-massacci
 feat: add differentiation for ContDiffMapSupportedIn Add a wrapper for `iteratedFDeriv` on `ContDiffMapSupportedIn` and related API. --- - [x] depends on: #30199 - [x] depends on: #30198 - [x] depends on: #30197 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-analysis 180/11 Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean,Mathlib/Topology/ContinuousMap/Bounded/Basic.lean 2 44 ['ADedecker', 'github-actions', 'grunweg', 'luigi-massacci', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] nobody
1-57992
1 day ago
1-63819
1 day ago
5-54709
5 days
31497 staroperator
author:staroperator
 feat(Algebra/Group): semigroup ideals This PR defines semigroup ideals; they are different from (in fact, a weaker form of) ring ideals. We prove that in a monoid whose algebraic order is well-quasi-order, all semigroup ideals are finitely generated, and the semigroup ideals satisfy the ascending chain condition. These definitions and results are useful in #27414. Note: Following `Ideal` with `Submodule`, `SemigroupIdeal M` is an `abbrev` of `SubMulAction M M`. Also, `Ideal.closure` is a re-definition of `SubMulAction.closure` and `Ideal.FG` is defeq to `SubMulAction.FG` but unfolds more nicely. --- - [x] depends on: #31517 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
 194/0 Mathlib.lean,Mathlib/Algebra/Group/Ideal.lean,Mathlib/Algebra/Order/Group/Ideal.lean 3 24 ['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'staroperator'] nobody
1-43368
1 day ago
1-57823
1 day ago
2-78684
2 days
31273 euprunin
author:euprunin
 chore(MeasureTheory/MeasurableSpace): golf `measurableSet_generateFrom_singleton_iff` using `grind` ---
Show trace profiling of measurableSet_generateFrom_singleton_iff: 70 ms before, 91 ms after ### Trace profiling of `measurableSet_generateFrom_singleton_iff` before PR 31273 ```diff diff --git a/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean b/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean index baf5299a16..fb8e3fc16d 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean @@ -42,6 +42,7 @@ end MeasurableSpace namespace MeasureTheory +set_option trace.profiler true in theorem measurableSet_generateFrom_singleton_iff {s t : Set α} : MeasurableSet[MeasurableSpace.generateFrom {s}] t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ := by simp_rw [MeasurableSpace.generateFrom_singleton] ``` ``` ℹ [880/880] Built Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (1.2s) info: Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean:46:0: [Elab.async] [0.071352] elaborating proof of MeasureTheory.measurableSet_generateFrom_singleton_iff [Elab.definition.value] [0.069878] MeasureTheory.measurableSet_generateFrom_singleton_iff [Elab.step] [0.068734] simp_rw [MeasurableSpace.generateFrom_singleton] unfold MeasurableSet MeasurableSpace.MeasurableSet' MeasurableSpace.comap simp_rw [MeasurableSpace.measurableSet_top, true_and] constructor · rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · refine Or.inr <| Or.inr <| Or.inr <| subset_antisymm (subset_univ _) ?_ suffices x = univ by simp only [this, preimage_univ, subset_refl] refine subset_antisymm (subset_univ _) ?_ rw [univ_eq_true_false] rintro - (rfl | rfl) · assumption · assumption · have hx : x = { True } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ by_contra hpneg rw [eq_iff_iff, iff_true, ← false_iff] at hpneg exact hF (by convert hp) simp [hx] · by_cases hF : False ∈ x · have hx : x = { False } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hF⟩ grind refine Or.inr <| Or.inr <| Or.inl <| ?_ simp [hx, compl_def] · refine Or.inl <| subset_antisymm ?_ <| empty_subset _ suffices x ⊆ ∅ by rw [subset_empty_iff] at this simp only [this, preimage_empty, subset_refl] intro p hp fin_cases p · contradiction · contradiction · rintro (rfl | rfl | rfl | rfl) on_goal 1 => use ∅ on_goal 2 => use { True } on_goal 3 => use { False } on_goal 4 => use Set.univ all_goals simp [compl_def] [Elab.step] [0.068727] simp_rw [MeasurableSpace.generateFrom_singleton] unfold MeasurableSet MeasurableSpace.MeasurableSet' MeasurableSpace.comap simp_rw [MeasurableSpace.measurableSet_top, true_and] constructor · rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · refine Or.inr <| Or.inr <| Or.inr <| subset_antisymm (subset_univ _) ?_ suffices x = univ by simp only [this, preimage_univ, subset_refl] refine subset_antisymm (subset_univ _) ?_ rw [univ_eq_true_false] rintro - (rfl | rfl) · assumption · assumption · have hx : x = { True } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ by_contra hpneg rw [eq_iff_iff, iff_true, ← false_iff] at hpneg exact hF (by convert hp) simp [hx] · by_cases hF : False ∈ x · have hx : x = { False } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hF⟩ grind refine Or.inr <| Or.inr <| Or.inl <| ?_ simp [hx, compl_def] · refine Or.inl <| subset_antisymm ?_ <| empty_subset _ suffices x ⊆ ∅ by rw [subset_empty_iff] at this simp only [this, preimage_empty, subset_refl] intro p hp fin_cases p · contradiction · contradiction · rintro (rfl | rfl | rfl | rfl) on_goal 1 => use ∅ on_goal 2 => use { True } on_goal 3 => use { False } on_goal 4 => use Set.univ all_goals simp [compl_def] [Elab.step] [0.012541] simp_rw [MeasurableSpace.generateFrom_singleton] [Elab.step] [0.041180] · rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · refine Or.inr <| Or.inr <| Or.inr <| subset_antisymm (subset_univ _) ?_ suffices x = univ by simp only [this, preimage_univ, subset_refl] refine subset_antisymm (subset_univ _) ?_ rw [univ_eq_true_false] rintro - (rfl | rfl) · assumption [… 112 lines omitted …] · assumption · assumption · have hx : x = { True } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ by_contra hpneg rw [eq_iff_iff, iff_true, ← false_iff] at hpneg exact hF (by convert hp) simp [hx] [Elab.step] [0.028797] by_cases hF : False ∈ x · refine Or.inr <| Or.inr <| Or.inr <| subset_antisymm (subset_univ _) ?_ suffices x = univ by simp only [this, preimage_univ, subset_refl] refine subset_antisymm (subset_univ _) ?_ rw [univ_eq_true_false] rintro - (rfl | rfl) · assumption · assumption · have hx : x = { True } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ by_contra hpneg rw [eq_iff_iff, iff_true, ← false_iff] at hpneg exact hF (by convert hp) simp [hx] [Elab.step] [0.025079] · have hx : x = { True } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ by_contra hpneg rw [eq_iff_iff, iff_true, ← false_iff] at hpneg exact hF (by convert hp) simp [hx] [Elab.step] [0.025059] have hx : x = { True } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ by_contra hpneg rw [eq_iff_iff, iff_true, ← false_iff] at hpneg exact hF (by convert hp) simp [hx] [Elab.step] [0.025057] have hx : x = { True } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ by_contra hpneg rw [eq_iff_iff, iff_true, ← false_iff] at hpneg exact hF (by convert hp) simp [hx] [Elab.step] [0.015096] simp [hx] [Meta.synthInstance] [0.011997] ❌️ Nontrivial (Set α) [Elab.step] [0.011467] · by_cases hF : False ∈ x · have hx : x = { False } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hF⟩ grind refine Or.inr <| Or.inr <| Or.inl <| ?_ simp [hx, compl_def] · refine Or.inl <| subset_antisymm ?_ <| empty_subset _ suffices x ⊆ ∅ by rw [subset_empty_iff] at this simp only [this, preimage_empty, subset_refl] intro p hp fin_cases p · contradiction · contradiction [Elab.step] [0.011367] by_cases hF : False ∈ x · have hx : x = { False } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hF⟩ grind refine Or.inr <| Or.inr <| Or.inl <| ?_ simp [hx, compl_def] · refine Or.inl <| subset_antisymm ?_ <| empty_subset _ suffices x ⊆ ∅ by rw [subset_empty_iff] at this simp only [this, preimage_empty, subset_refl] intro p hp fin_cases p · contradiction · contradiction [Elab.step] [0.011363] by_cases hF : False ∈ x · have hx : x = { False } := by ext p refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hF⟩ grind refine Or.inr <| Or.inr <| Or.inl <| ?_ simp [hx, compl_def] · refine Or.inl <| subset_antisymm ?_ <| empty_subset _ suffices x ⊆ ∅ by rw [subset_empty_iff] at this simp only [this, preimage_empty, subset_refl] intro p hp fin_cases p · contradiction · contradiction Build completed successfully (880 jobs). ``` ### Trace profiling of `measurableSet_generateFrom_singleton_iff` after PR 31273 ```diff diff --git a/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean b/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean index baf5299a16..b67f37d372 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean @@ -42,6 +42,7 @@ end MeasurableSpace namespace MeasureTheory +set_option trace.profiler true in theorem measurableSet_generateFrom_singleton_iff {s t : Set α} : MeasurableSet[MeasurableSpace.generateFrom {s}] t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ := by simp_rw [MeasurableSpace.generateFrom_singleton] @@ -51,35 +52,14 @@ theorem measurableSet_generateFrom_singleton_iff {s t : Set α} : · rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x - · refine Or.inr <| Or.inr <| Or.inr <| subset_antisymm (subset_univ _) ?_ - suffices x = univ by simp only [this, preimage_univ, subset_refl] - refine subset_antisymm (subset_univ _) ?_ - rw [univ_eq_true_false] - rintro - (rfl | rfl) - · assumption - · assumption - · have hx : x = {True} := by - ext p - refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩ - by_contra hpneg - rw [eq_iff_iff, iff_true, ← false_iff] at hpneg - exact hF (by convert hp) - simp [hx] + · suffices x = univ by grind + grind [univ_eq_true_false] + · grind · by_cases hF : False ∈ x - · have hx : x = {False} := by - ext p - refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hF⟩ - grind - refine Or.inr <| Or.inr <| Or.inl <| ?_ - simp [hx, compl_def] - · refine Or.inl <| subset_antisymm ?_ <| empty_subset _ - suffices x ⊆ ∅ by - rw [subset_empty_iff] at this - simp only [this, preimage_empty, subset_refl] + · grind + · suffices x ⊆ ∅ by grind intro p hp - fin_cases p - · contradiction - · contradiction + fin_cases p <;> contradiction · rintro (rfl | rfl | rfl | rfl) on_goal 1 => use ∅ on_goal 2 => use {True} ``` ``` ℹ [880/880] Built Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (1.2s) info: Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean:46:0: [Elab.async] [0.092756] elaborating proof of MeasureTheory.measurableSet_generateFrom_singleton_iff [Elab.definition.value] [0.091377] MeasureTheory.measurableSet_generateFrom_singleton_iff [Elab.step] [0.090497] simp_rw [MeasurableSpace.generateFrom_singleton] unfold MeasurableSet MeasurableSpace.MeasurableSet' MeasurableSpace.comap simp_rw [MeasurableSpace.measurableSet_top, true_and] constructor · rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind · by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction · rintro (rfl | rfl | rfl | rfl) on_goal 1 => use ∅ on_goal 2 => use { True } on_goal 3 => use { False } on_goal 4 => use Set.univ all_goals simp [compl_def] [Elab.step] [0.090489] simp_rw [MeasurableSpace.generateFrom_singleton] unfold MeasurableSet MeasurableSpace.MeasurableSet' MeasurableSpace.comap simp_rw [MeasurableSpace.measurableSet_top, true_and] constructor · rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind · by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction · rintro (rfl | rfl | rfl | rfl) on_goal 1 => use ∅ on_goal 2 => use { True } on_goal 3 => use { False } on_goal 4 => use Set.univ all_goals simp [compl_def] [Elab.step] [0.012749] simp_rw [MeasurableSpace.generateFrom_singleton] [Elab.step] [0.062153] · rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind · by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.062134] rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind · by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.062131] rintro ⟨x, rfl⟩ by_cases hT : True ∈ x · by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind · by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.031421] · by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind [Elab.step] [0.031410] by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind [Elab.step] [0.031407] by_cases hF : False ∈ x · suffices x = univ by grind grind [univ_eq_true_false] · grind [Elab.step] [0.019456] · suffices x = univ by grind grind [univ_eq_true_false] [Elab.step] [0.019448] suffices x = univ by grind grind [univ_eq_true_false] [Elab.step] [0.019444] suffices x = univ by grind grind [univ_eq_true_false] [Elab.step] [0.010344] grind [univ_eq_true_false] [Elab.step] [0.011419] · grind [Elab.step] [0.011411] grind [Elab.step] [0.011407] grind [Elab.step] [0.011402] grind [Elab.step] [0.029820] · by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.029812] by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.029808] by_cases hF : False ∈ x · grind · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.011217] · grind [Elab.step] [0.011211] grind [Elab.step] [0.011208] grind [Elab.step] [0.011203] grind [Elab.step] [0.017927] · suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.017920] suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.017914] suffices x ⊆ ∅ by grind intro p hp fin_cases p <;> contradiction [Elab.step] [0.014460] suffices x ⊆ ∅ by grind [Elab.step] [0.014455] refine_lift suffices x ⊆ ∅ by grind; ?_ [Elab.step] [0.014451] focus (refine no_implicit_lambda% (suffices x ⊆ ∅ by grind; ?_); rotate_right) [Elab.step] [0.014447] (refine no_implicit_lambda% (suffices x ⊆ ∅ by grind; ?_); rotate_right) [Elab.step] [0.014445] (refine no_implicit_lambda% (suffices x ⊆ ∅ by grind; ?_); rotate_right) [Elab.step] [0.014442] (refine no_implicit_lambda% (suffices x ⊆ ∅ by grind; ?_); rotate_right) [Elab.step] [0.014440] refine no_implicit_lambda% (suffices x ⊆ ∅ by grind; ?_); rotate_right [Elab.step] [0.014438] refine no_implicit_lambda% (suffices x ⊆ ∅ by grind; ?_); rotate_right [Elab.step] [0.014428] refine no_implicit_lambda% (suffices x ⊆ ∅ by grind; ?_) [Elab.step] [0.013889] grind [Elab.step] [0.013885] grind [Elab.step] [0.013879] grind Build completed successfully (880 jobs). ```
--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) 		maintainer-merge t-measure-probability 6/27 Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean 1 3 ['EtienneC30', 'github-actions'] EtienneC30
assignee:EtienneC30
1-41936
1 day ago
1-41936
1 day ago
8-83381
8 days
31398 YaelDillies
author:YaelDillies
 feat(MeasureTheory/Measure): `comap_apply` version for measurable equivs This one is stated in terms of the preimage of the inverse, which is sometimes (but not always!) more useful than the image of the forward map. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-measure-probability 13/0 Mathlib/MeasureTheory/Measure/Restrict.lean 1 4 ['EtienneC30', 'YaelDillies', 'github-actions'] EtienneC30
assignee:EtienneC30
1-40781
1 day ago
1-40806
1 day ago
5-33993
5 days
31278 ADedecker
author:ADedecker
 feat: approximate continuous functions by smooth functions This is motivated by #31079, and adapted from [this lemma](https://github.com/leanprover-community/sphere-eversion/blob/master/SphereEversion/ToMathlib/ExistsOfConvex.lean#L213) in the Sphere Eversion project. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-analysis t-differential-geometry 157/0 Mathlib.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/FDeriv/Const.lean,Mathlib/Analysis/Convex/Basic.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean,Mathlib/Geometry/Manifold/SmoothApprox.lean 7 36 ['ADedecker', 'github-actions', 'grunweg', 'mcdoll', 'sgouezel'] grunweg
assignee:grunweg
1-35442
1 day ago
7-60030
7 days ago
8-48995
8 days
30650 JovanGerb
author:JovanGerb
 perf(reassoc, to_app, elementwise): don't pass the same proof to the kernel again In `reassoc`, `to_app`, `elementwise`, the proof of the original lemma was being used to prove the modified lemma. This is silly, because the modified lemma can be proved using the original lemma directly. Hence, this PR modifies `addRelatedDecl` to include this optimization. Previously, `addRelatedDecl` would pass around both the type and the value of the original declaration. This was necessary, because the inferred type of the value might not be identical to the type it is given. Now this is not necessary anymore, because the type of the constant is exactly the type that it is given, so the type can always be obtained with `inferType`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta 19/21 Mathlib/Tactic/CategoryTheory/Elementwise.lean,Mathlib/Tactic/CategoryTheory/Reassoc.lean,Mathlib/Tactic/CategoryTheory/ToApp.lean,Mathlib/Util/AddRelatedDecl.lean 4 13 ['JovanGerb', 'dwrensha', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'plp127'] dwrensha
assignee:dwrensha
1-27737
1 day ago
1-69253
1 day ago
26-58555
26 days
31535 ADedecker
author:ADedecker
 feat: small tweaks to `PointwiseConvergenceCLM` These are small suggestions I would have made about #11496: - add a `IsUniformEmbedding` variant of `isEmbedding_coeFn` - add a `ContinuousEvalConst` instance using [UniformConvergenceCLM.continuousEvalConst](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/Module/StrongTopology.html#UniformConvergenceCLM.continuousEvalConst) - use said instance to golf continuity in `evalCLM` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 16/11 Mathlib/Topology/Algebra/Module/PointwiseConvergence.lean 1 3 ['github-actions', 'mcdoll'] nobody
1-25338
1 day ago
1-25338
1 day ago
1-80598
1 day
31546 RemyDegenne
author:RemyDegenne
 feat: MeasurableSet.iff Add two lemmas: `MeasurableSet.imp (hs : MeasurableSet {x | p x}) (ht : MeasurableSet {x | q x}) : MeasurableSet {x | p x → q x}` `MeasurableSet.iff (hs : MeasurableSet {x | p x}) (ht : MeasurableSet {x | q x}) : MeasurableSet {x | p x ↔ q x}` From the LeanBandits project. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-measure-probability 14/0 Mathlib/MeasureTheory/MeasurableSpace/Defs.lean 1 3 ['EtienneC30', 'github-actions'] nobody
0-76586
21 hours ago
0-76586
21 hours ago
1-70528
1 day
31544 RemyDegenne
author:RemyDegenne
 feat: add `MeasureTheory.Measure.integrable_comp_iff` Necessary and sufficient condition for `Integrable f (κ ∘ₘ μ)`, integrability with respect to the composition of a kernel and a measure. Special case of `ProbabilityTheory.integrable_comp_iff`, which is about composition of two kernels. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-measure-probability 8/0 Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean 1 2 ['EtienneC30', 'github-actions'] nobody
0-72810
20 hours ago
0-72810
20 hours ago
1-72210
1 day
31451 jsm28
author:jsm28
 feat(Analysis/Convex/Combination): `centerMass_const`, `centerMass_congr` Add the lemma: ```lean lemma Finset.centerMass_const (hw : ∑ j ∈ t, w j ≠ 0) (c : E) : t.centerMass w (Function.const _ c) = c := by ``` along with various congruence lemmas that help with applying this in cases where the points are constant for the nonzero weights in `t`, but not necessarily everywhere. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-convex-geometry maintainer-merge t-analysis 28/0 Mathlib/Analysis/Convex/Combination.lean 1 4 ['Ruben-VandeVelde', 'github-actions', 'j-loreaux', 'jsm28'] nobody
0-72217
20 hours ago
0-72217
20 hours ago
4-1386
4 days
31493 jsm28
author:jsm28
 feat(Geometry/Euclidean/Incenter): `incenter_mem_interior` Add a direct statement that the incenter of a simplex lies in its interior (along with factoring out a lemma `excenterWeights_empty_pos` that turns out to be useful several times in its proof). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-euclidean-geometry 21/2 Mathlib/Geometry/Euclidean/Incenter.lean 1 3 ['Ruben-VandeVelde', 'github-actions'] nobody
0-71128
19 hours ago
0-71975
19 hours ago
3-21984
3 days
30913 eric-wieser
author:eric-wieser
 feat(Computability/Language): add subtraction notation Defining `-` as set difference seems like a natural thing to do when `+` is set union. The fact that this definition satisfies `OrderedSub` seems to be a good signal that it is a good idea. --- - [x] depends on: #30912 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-computability 22/0 Mathlib/Computability/Language.lean 1 9 ['YaelDillies', 'chenson2018', 'ctchou', 'eric-wieser', 'github-actions', 'jessealama', 'mathlib4-dependent-issues-bot'] nobody
0-35588
9 hours ago
7-68538
7 days ago
14-30572
14 days
31510 JovanGerb
author:JovanGerb
 feat(contrapose): cancel negations, and support `↔` This PR introduces two features for `contrapose`: - `contrapose` applied to a goal `p ↔ q` creates the goal `¬p ↔ ¬q`. - Instead of creating double negations, contrapose will try to cancel out double negations that it creates. This will allow for replacing some occurrences of `contrapose!` with `contrapose` (TODO: write a linter for this?). It also allows avoiding classical logic in some cases. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/RFC.3A.20contrapose.20for.20.60a.20.E2.86.94.20b.60/with/554945103) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta 172/18 Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean,Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean,Mathlib/RingTheory/Localization/Integral.lean,Mathlib/RingTheory/Valuation/ValuationRing.lean,Mathlib/Tactic/Contrapose.lean,MathlibTest/Contrapose.lean 6 21 ['JovanGerb', 'github-actions', 'grunweg', 'leanprover-bot'] nobody
0-33473
9 hours ago
1-69632
1 day ago
1-82418
1 day
31149 riccardobrasca
author:riccardobrasca
 feat: power series over a noetherian ring is noetherian We add that the power series ring over a noetherian ring is noetherian. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory maintainer-merge 287/3 Mathlib.lean,Mathlib/Algebra/Module/SpanRank.lean,Mathlib/RingTheory/PowerSeries/Ideal.lean,Mathlib/RingTheory/PowerSeries/Trunc.lean,docs/references.bib 5 40 ['copilot-pull-request-reviewer', 'erdOne', 'github-actions', 'riccardobrasca', 'yapudpill'] erdOne
assignee:erdOne
0-26089
7 hours ago
4-36030
4 days ago
10-85945
10 days
31384 harahu
author:harahu
 doc(Archive): ensure only a single H1 header per file This PR ensures we only have a single H1 header per lean file in the Archive subdirectory. We do this for the following reasons: - Having more than one H1 header per file is likely to hamper both assistive technologies and SEO, since it introduces ambiguity about what the title of the resulting webpage actually is. - The [documentation style guide](https://leanprover-community.github.io/contribute/doc.html) asks for the title of the file to be H1, any other header in the file-level docstring to be H2, and sectioning headers to be H3. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) IMO maintainer-merge 16/16 Archive/Imo/Imo1975Q1.lean,Archive/Imo/Imo1985Q2.lean,Archive/Imo/Imo1994Q1.lean,Archive/Imo/Imo1997Q3.lean,Archive/Imo/Imo2001Q3.lean,Archive/Imo/Imo2001Q4.lean,Archive/Imo/Imo2001Q5.lean,Archive/Imo/Imo2005Q3.lean,Archive/Imo/Imo2008Q2.lean,Archive/Imo/Imo2008Q3.lean,Archive/Imo/Imo2008Q4.lean,Archive/Imo/Imo2011Q3.lean,Archive/Imo/Imo2013Q1.lean,Archive/Imo/Imo2013Q5.lean,Archive/Imo/Imo2015Q6.lean,Archive/Imo/Imo2021Q1.lean 16 3 ['github-actions', 'jsm28'] jsm28
assignee:jsm28
0-25820
7 hours ago
0-25820
7 hours ago
5-54388
5 days

PRs blocked on a zulip discussion

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
15649 TpmKranz
author:TpmKranz
 feat(Computability): introduce Generalised NFA as bridge to Regular Expression Lays the groundwork for a proof of equivalence of NFA and RE, w.r.t. described language. Actual connection to NFA comes later, after the groundwork for the opposite direction has been laid. Second chunk of #12648 --- - [x] depends on: #15647 [Data.FinEnum.Option unchanged since then] [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor awaiting-author 298/0 Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib 5 6 ['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'trivial1711'] nobody
192-35259
6 months ago
192-35268
6 months ago
23-54870
23 days
20648 anthonyde
author:anthonyde
 feat: formalize regular expression -> εNFA The file `Computability/RegularExpressionsToEpsilonNFA.lean` contains a formal definition of Thompson's method for constructing an `εNFA` from a `RegularExpression` and a proof of its correctness. --- - [x] depends on: #20644 - [x] depends on: #20645 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor 490/0 Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib 3 5 ['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'qawbecrdtey'] nobody
192-34570
6 months ago
192-35205
6 months ago
75-77754
75 days
20238 maemre
author:maemre
 feat(Computability/DFA): Closure of regular languages under some set operations This shows that regular languages are closed under complement and intersection by constructing DFAs for them. --- Closure under all other operations will be proved when someone adds the proof for DFA<->regular expression equivalence, so they are not part of this PR. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor awaiting-author 159/0 Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean 2 59 ['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'meithecatte', 'urkud'] EtienneC30
assignee:EtienneC30
163-1030
5 months ago
192-35169
6 months ago
48-67492
48 days
23929 meithecatte
author:meithecatte
 feat(Computability/NFA): improve bound on pumping lemma --- - [x] depends on: #25321 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor 101/10 Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean 2 41 ['YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte'] nobody
159-44821
5 months ago
159-44822
5 months ago
34-10595
34 days
30526 SnirBroshi
author:SnirBroshi
 chore(Logic/Relation): use `Subrelation` to state theorems chore(Logic/Relation): replace every `∀ x y, r x y → r' x y` with `Subrelation r r'` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip 79/73 Mathlib/CategoryTheory/IsConnected.lean,Mathlib/CategoryTheory/Limits/Types/Filtered.lean,Mathlib/CategoryTheory/Limits/Types/Shapes.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/GroupTheory/FreeGroup/Basic.lean,Mathlib/Logic/Relation.lean,Mathlib/Order/Interval/Finset/Basic.lean 7 4 ['SnirBroshi', 'github-actions', 'thorimur', 'vihdzp'] thorimur
assignee:thorimur
22-26607
22 days ago
22-26640
22 days ago
8-76821
8 days
30668 astrainfinita
author:astrainfinita
 feat: `QuotLike` This typeclass is primarily for use by type synonyms of `Quot` and `Quotient`. Using `QuotLike` API for type synonyms of `Quot` and `Quotient` will avoid defeq abuse caused by directly using `Quot` and `Quotient` APIs. This PR also adds some typeclasses to support different ways to find the quotient map that should be used. See the documentation comments of these typeclasses for examples of usage. --- It's not a typical design to use these auxiliary typeclasses and term elaborators, but I haven't found a better way to support these notations. Some of the naming may need to be discussed. For example: - `⟦·⟧` is currently called `mkQ` in names. This distinguishes it from other `.mk`s and makes it possible to write the quotient map as `mkQ` `mkQ'` `mkQ_ h`. But this will also require changing the old lemma names. - It would be helpful if the names of new type classes explained their functionality better. - Maybe `QuotLike` isn't the appropriate name. It may suggest that this typeclass is similar to `FunLike` and `SetLike`, but it is not. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/migrate.20to.20.60QuotLike.60.20API) This PR continues the work from #16421. Original PR: https://github.com/leanprover-community/mathlib4/pull/16421 t-data awaiting-zulip RFC awaiting-author 743/0 Mathlib.lean,Mathlib/Data/QuotLike.lean,MathlibTest/QuotLike.lean 3 14 ['YaelDillies', 'astrainfinita', 'github-actions', 'vihdzp'] nobody
20-1043
20 days ago
20-1043
20 days ago
0-81
1 minute
30902 adomani
author:adomani
 chore: longLine warnings happen starting at the 101st character Right now, the longLine linter warning spans the whole line. This PR changes the behaviour and the warning only covers the characters exceeding the 100 character limit. Previous discussion: [#general > error lens in lean4 @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/error.20lens.20in.20lean4/near/547074537) Specific thread: [#mathlib4 > Restrict longLine warning to exceeding characters @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Restrict.20longLine.20warning.20to.20exceeding.20characters/near/547081669) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-linter 1/1 Mathlib/Tactic/Linter/Style.lean 1 1 ['github-actions'] nobody
19-41385
19 days ago
19-41642
19 days ago
0-132
2 minutes
11800 JADekker
author:JADekker
 feat : Define KappaLindelöf spaces Define KappaLindelöf spaces by following the first one-third of the API for Lindelöf spaces. The remainder will be added in a future PR. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-topology merge-conflict please-adopt 301/2 Mathlib.lean,Mathlib/Topology/Compactness/KappaLindelof.lean,Mathlib/Topology/Compactness/Lindelof.lean 3 38 ['ADedecker', 'JADekker', 'PatrickMassot', 'StevenClontz', 'adomani', 'github-actions', 'grunweg', 'kim-em', 'urkud'] nobody
424-12292
1 year ago
424-34267
1 year ago
119-10687
119 days
17623 FR-vdash-bot
author:FR-vdash-bot
 feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas Some lemmas in `Algebra.Order.GroupWithZero.Unbundled` have incorrect or unsatisfactory names, or assumptions that can be omitted using `ZeroLEOneClass`. The lemmas added in this PR are versions of existing lemmas that use the correct or better name or `ZeroLEOneClass` to omit an assumption. The original lemmas will be deprecated in #17593. | New name | Old name | |-------------------------|-------------------------| | `mul_le_one_left₀` | `Left.mul_le_one_of_le_of_le` | | `mul_lt_one_of_le_of_lt_left₀` (`0 ≤ ·` version) / `mul_lt_one_of_le_of_lt_of_pos_left` | `Left.mul_lt_of_le_of_lt_one_of_pos` | | `mul_lt_one_of_lt_of_le_left₀` | `Left.mul_lt_of_lt_of_le_one_of_nonneg` | | `mul_le_one_right₀` | `Right.mul_le_one_of_le_of_le` | | `mul_lt_one_of_lt_of_le_right₀` (`0 ≤ ·` version) / `mul_lt_one_of_lt_of_le_of_pos_right` | `Right.mul_lt_one_of_lt_of_le_of_pos` | | `mul_lt_one_of_le_of_lt_right₀` | `Right.mul_lt_one_of_le_of_lt_of_nonneg` | The following lemmas use `ZeroLEOneClass`. | New name | Old name | |-------------------------|-------------------------| | `(Left.)one_le_mul₀` | `Left.one_le_mul_of_le_of_le` | | `Left.one_lt_mul_of_le_of_lt₀` | `Left.one_lt_mul_of_le_of_lt_of_pos` | | `Left.one_lt_mul_of_lt_of_le₀` | `Left.lt_mul_of_lt_of_one_le_of_nonneg` / `one_lt_mul_of_lt_of_le` (still there) | | `(Left.)one_lt_mul₀` | | | `Right.one_le_mul₀` | `Right.one_le_mul_of_le_of_le` | | `Right.one_lt_mul_of_lt_of_le₀` | `Right.one_lt_mul_of_lt_of_le_of_pos` | | `Right.one_lt_mul_of_le_of_lt₀` | `Right.one_lt_mul_of_le_of_lt_of_nonneg` / `one_lt_mul_of_le_of_lt` (still there) / `one_lt_mul` (still there) | | `Right.one_lt_mul₀` | `Right.one_lt_mul_of_lt_of_lt` | --- Split from #17593. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-order t-algebra merge-conflict
label:t-algebra$
 146/44 Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean 2 11 ['FR-vdash-bot', 'YaelDillies', 'github-actions', 'j-loreaux'] nobody
358-71942
11 months ago
358-71942
11 months ago
33-64877
33 days
8370 eric-wieser
author:eric-wieser
 refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` This argument is still needed for almost all the lemmas, which means it can longer be found by unification. We keep around `expSeries 𝕂 A`, as it's needed for talking about the radius of convergence over different base fields. This is a prerequisite for #8372, as we can't merge the functions until they have the same interface.\ Zulip thread: [#mathlib4 > Real.exp @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Real.2Eexp/near/401602245) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This is started from the mathport output on https://github.com/leanprover-community/mathlib/pull/19244 awaiting-zulip t-analysis merge-conflict 432/387 Mathlib/Analysis/CStarAlgebra/Exponential.lean,Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean,Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean,Mathlib/Analysis/NormedSpace/DualNumber.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean,Mathlib/Analysis/SpecialFunctions/Exponential.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean 11 29 ['YaelDillies', 'eric-wieser', 'girving', 'github-actions', 'j-loreaux', 'kbuzzard', 'leanprover-community-bot-assistant', 'urkud'] nobody
203-27319
6 months ago
214-55949
7 months ago
29-60989
29 days
17458 urkud
author:urkud
 refactor(Algebra/Group): make `IsUnit` a typeclass Also change some lemmas to assume `[IsUnit _]` instead of `[Invertible _]`. Motivated by potential non-defeq diamonds in #14986, see also [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Invertible.20and.20data) I no longer plan to merge this PR, but I'm going to cherry-pick some changes to a new PR before closing this one. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-algebra merge-conflict
label:t-algebra$
 82/72 Mathlib/Algebra/CharP/Invertible.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/Algebra/Polynomial/Degree/Units.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Affine/Isometry.lean,Mathlib/Analysis/Normed/Ring/Units.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SeparableDegree.lean,Mathlib/GroupTheory/Submonoid/Inverses.lean,Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean,Mathlib/LinearAlgebra/AffineSpace/Combination.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean,Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean,Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean,Mathlib/NumberTheory/MulChar/Basic.lean,Mathlib/RingTheory/Localization/NumDen.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean,Mathlib/RingTheory/Valuation/Basic.lean 26 12 ['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'urkud'] nobody
132-15568
4 months ago
132-15568
4 months ago
0-66650
18 hours
25218 kckennylau
author:kckennylau
 feat(AlgebraicGeometry): Tate normal form of elliptic curves --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip new-contributor t-algebraic-geometry merge-conflict 291/26 Mathlib.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Modular/TateNormalForm.lean,Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean,Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean 5 31 ['MichaelStollBayreuth', 'Multramate', 'acmepjz', 'github-actions', 'grunweg', 'kckennylau', 'leanprover-community-bot-assistant'] nobody
132-14406
4 months ago
132-14407
4 months ago
6-51040
6 days
28803 astrainfinita
author:astrainfinita
 refactor: unbundle algebra from `ENormed*` Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`. This PR continues the work from #23961. - Change `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` so they no longer carry algebraic data. - Deprecate `ESeminormed(Add)CommMonoid` and `ENormed(Add)CommMonoid` in favor of `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` with a commutative algebraic typeclass. |Old|New| |---|---| | `[ESeminormed(Add)(Comm)Monoid E]` | `[(Add)(Comm)Monoid E] [ESeminormed(Add)Monoid E]` | | `[ENormed(Add)(Comm)Monoid]` | `[(Add)(Comm)Monoid E] [ENormed(Add)Monoid]` | See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2328803.20refactor.3A.20unbundle.20algebra.20from.20.60ENormed*.60/with/536024350) ------------ - [x] depends on: #28813 awaiting-zulip slow-typeclass-synthesis t-algebra t-analysis merge-conflict
label:t-algebra$
 80/63 Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/Normed/Group/InfiniteSum.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean,Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean,Mathlib/MeasureTheory/Function/L1Space/Integrable.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean,Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean,Mathlib/MeasureTheory/Integral/IntegrableOn.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean 14 28 ['astrainfinita', 'bryangingechen', 'github-actions', 'grunweg', 'kbuzzard', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib-bors', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel'] grunweg
assignee:grunweg
72-30051
2 months ago
72-30052
2 months ago
0-20585
5 hours
28925 grunweg
author:grunweg
 chore: remove `linear_combination'` tactic When `linear_combination` was refactored in #15899, the old code was kept as the `linear_combination'` tactic, for easier migration. The consensus of the zulip discussion ([#mathlib4 > Narrowing the scope of `linear_combination` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Narrowing.20the.20scope.20of.20.60linear_combination.60/near/470237816)) was to wait, and "revisit this once people have experienced the various tactics in practice". One year later, the old tactic has almost no uses: it is unused in mathlib; [searching on github](https://github.com/search?q=linear_combination%27%20path%3A*.lean&type=code) yields 37 hits --- all of which are in various forks of mathlib. Thus, removing this tactic seems appropriate. --- Do not merge before the zulip discussion has concluded! [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed awaiting-zulip merge-conflict 0/564 Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/LinearCombination'.lean,Mathlib/Tactic/Linter/UnusedTactic.lean,MathlibTest/linear_combination'.lean 5 4 ['euprunin', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot'] nobody
29-7261
29 days ago
29-7262
29 days ago
0-1
1 second
22361 rudynicolop
author:rudynicolop
 feat(Computability/NFA): nfa closure properties Add the closure properties union, intersection and reversal for NFA. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor merge-conflict awaiting-author 218/2 Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean 2 91 ['EtienneC30', 'b-mehta', 'ctchou', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] EtienneC30
assignee:EtienneC30
10-16951
10 days ago
178-56901
5 months ago
39-67601
39 days
30150 imbrem
author:imbrem
 feat(CategoryTheory/Monoidal): to_additive for MonoidalCategory Add `AddMonoidalCategory`, the additive version of `MonoidalCategory`. To get this to work, I needed to _remove_ the `to_additive` attributes in `Discrete.lean`, since existing code relies on the `AddMonoid M → MonoidalCategory M` instance. For now, we simply implement the additive variants by hand instead. --- As discussed in #28718; I added an `AddMonoidalCategory` struct and tagged `MonoidalCategory` with `to_additive`, along with the lemmas in `Category.lean`. I think this is the right approach, since under this framework the "correct" additive version of `Discrete.lean` would be mapping an `AddMonoid` to an `AddMonoidalCategory`. Next steps would be to: - Make `monoidal_coherence` and `coherence` support `AddMonoidalCategory` - Add `CocartesianMonoidalCategory` extending `AddMonoidalCategory` [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import awaiting-zulip new-contributor t-category-theory t-meta merge-conflict 444/125 Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Tactic/ToAdditive/GuessName.lean 3 22 ['JovanGerb', 'YaelDillies', 'github-actions', 'imbrem', 'mathlib4-merge-conflict-bot'] nobody
1-18135
1 day ago
1-18135
1 day ago
1-18384
1 day
15651 TpmKranz
author:TpmKranz
 feat(Computability/NFA): operations for Thompson's construction Lays the groundwork for a proof of equivalence of RE and NFA, w.r.t. described language. Actual connection to REs comes later, after the groundwork for the opposite direction has been laid. Third chunk of #12648 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor merge-conflict awaiting-author 307/5 Mathlib/Computability/NFA.lean 1 16 ['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] nobody
0-27868
7 hours ago
178-57826
5 months ago
45-84611
45 days
24614 JovanGerb
author:JovanGerb
 chore: rename field `inf` to `min` in `Lattice` As suggested by @eric-wieser, this PR renames the `sup` and `inf` fields in `Lattice` to `max` and `min`. This means that we now can extend `Lattice` and `LinearOrder` simultaneously without ending up with duplicate fields. This should be implemented in a future PR for existing classes like `CompleteLinearOrder`. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60sup.60.2F.60inf.60.20or.20.60max.60.2F.60min.60.20for.20set.20interval.20lemmas.3F) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-order merge-conflict 181/187 Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/Algebra/Group/Subgroup/Lattice.lean,Mathlib/Algebra/Group/Submonoid/Basic.lean,Mathlib/Algebra/Group/Subsemigroup/Basic.lean,Mathlib/Algebra/Lie/Subalgebra.lean,Mathlib/Algebra/Module/Submodule/Lattice.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/Kleene.lean,Mathlib/Algebra/Order/Ring/Idempotent.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Algebra/Tropical/Lattice.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean,Mathlib/Analysis/BoxIntegral/Box/Basic.lean,Mathlib/Analysis/BoxIntegral/Partition/Basic.lean,Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean,Mathlib/Analysis/Normed/Group/Seminorm.lean,Mathlib/Analysis/NormedSpace/ENormedSpace.lean,Mathlib/Analysis/NormedSpace/MStructure.lean,Mathlib/Analysis/Seminorm.lean,Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean,Mathlib/CategoryTheory/Sites/Coverage.lean,Mathlib/CategoryTheory/Sites/Grothendieck.lean,Mathlib/CategoryTheory/Sites/Pretopology.lean,Mathlib/CategoryTheory/Sites/Sieves.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/CategoryTheory/Subpresheaf/Basic.lean,Mathlib/Combinatorics/Digraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean,Mathlib/Computability/Reduce.lean,Mathlib/Data/DFinsupp/Order.lean,Mathlib/Data/Finset/Lattice/Basic.lean,Mathlib/Data/Multiset/UnionInter.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Data/PEquiv.lean,Mathlib/Data/Real/Basic.lean,Mathlib/Data/Semiquot.lean,Mathlib/Data/Set/Basic.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/Data/Sum/Lattice.lean,Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean,Mathlib/Geometry/Manifold/ChartedSpace.lean,Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean,Mathlib/LinearAlgebra/LinearPMap.lean,Mathlib/MeasureTheory/Function/AEEqFun.lean,Mathlib/MeasureTheory/Function/SimpleFunc.lean,Mathlib/ModelTheory/Substructures.lean,Mathlib/Order/BooleanSubalgebra.lean,Mathlib/Order/Booleanisation.lean,Mathlib/Order/CompleteLattice/Defs.lean,Mathlib/Order/Concept.lean,Mathlib/Order/ConditionallyCompleteLattice/Defs.lean,Mathlib/Order/Copy.lean,Mathlib/Order/Filter/Basic.lean,Mathlib/Order/Filter/Germ/Basic.lean,Mathlib/Order/FixedPoints.lean,Mathlib/Order/GaloisConnection/Basic.lean,Mathlib/Order/Heyting/Basic.lean,Mathlib/Order/Hom/Order.lean,Mathlib/Order/Ideal.lean,Mathlib/Order/Interval/Basic.lean,Mathlib/Order/Lattice.lean,Mathlib/Order/Partition/Finpartition.lean,Mathlib/Order/Preorder/Finsupp.lean,Mathlib/Order/PropInstances.lean,Mathlib/Order/Sublattice.lean,Mathlib/Order/WithBot.lean,Mathlib/Probability/Process/Filtration.lean,Mathlib/RingTheory/Congruence/Basic.lean,Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/Finiteness/Small.lean,Mathlib/RingTheory/NonUnitalSubring/Basic.lean,Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean,Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean,Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean,Mathlib/RingTheory/Valuation/ValuationSubring.lean,Mathlib/Topology/Algebra/Group/GroupTopology.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean,Mathlib/Topology/Category/TopCat/OpenNhds.lean,Mathlib/Topology/LocallyFinsupp.lean,Mathlib/Topology/MetricSpace/BundledFun.lean,Mathlib/Topology/UniformSpace/Basic.lean 84 15 ['JovanGerb', 'bryangingechen', 'eric-wieser', 'github-actions', 'j-loreaux', 'leanprover-bot', 'leanprover-community-bot-assistant', 'leanprover-community-mathlib4-bot'] Vierkantor
assignee:Vierkantor
0-17917
4 hours ago
2-36318
2 days ago
24-8021
24 days
17518 grunweg
author:grunweg
 feat: lint on declarations mentioning `Invertible` or `Unique` Using the same infrastructure as for #10235. Depends on that PR to land first, and also (for the first lint) a zulip discussion if that change is desired/about the best way to enact it. --- - [ ] depends on: #10235 awaiting-zulip t-linter merge-conflict blocked-by-other-PR 149/7 Mathlib.lean,Mathlib/Algebra/MvPolynomial/PDeriv.lean,Mathlib/Computability/Halting.lean,Mathlib/Computability/TuringMachine.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/GroupTheory/Perm/DomMulAct.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/NumberTheory/JacobiSum/Basic.lean,Mathlib/Order/Heyting/Regular.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/UnusedAssumptionInType.lean 13 3 ['github-actions', 'mathlib4-dependent-issues-bot', 'mergify'] nobody
376-52411
1 year ago
402-40933
1 year ago*
0-0
0 seconds*
15654 TpmKranz
author:TpmKranz
 feat(Computability): language-preserving maps between NFA and RE Map REs to NFAs via Thompson's construction and NFAs to REs using GNFAs Last chunk of #12648 --- - [ ] depends on: #15651 - [ ] depends on: #15649 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor merge-conflict blocked-by-other-PR 985/2 Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Data/FinEnum/Option.lean,docs/references.bib 7 3 ['github-actions', 'leanprover-community-mathlib4-bot', 'meithecatte'] nobody
192-35219
6 months ago
192-35224
6 months ago
0-179
2 minutes

PRs on the review queue labelled 'tech debt' or 'longest-pole'

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
30107 grunweg
author:grunweg
 chore: track occurrences of 'nonrec' as technical debt Matches leanprover-community/leanprover-community.github.io#689: only merge when that is deemed a good idea. -------- TODO: make the count more robust, for instance count all occurrences of "^nonrec " plus those of "^[private|protected] nonrec ". --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) tech debt CI 1/0 scripts/technical-debt-metrics.sh 1 1 ['github-actions'] robertylewis
assignee:robertylewis
36-26090
1 month ago
43-85378
1 month ago
43-85356
43 days