feat(Tactic): convert now discharges side goals at reducible transparency by Vierkantor · Pull Request #39039 · leanprover-community/mathlib4

Vierkantor · 2026-05-07T15:06:28Z

This PR changes the postCongr! discharge step of the convert tactic to operate at reducible transparency by default, just like the preCongr! step. This should make the behaviour more predictable since it does not unfold quite as much. convert_to and ac_change get a similar modification, since they are macros on top of convert.

To get back the old behaviour and work at default transparency, write convert!. To make Mathlib not break due to this change, we replace all occurrences of convert with convert! in the next commit.

Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20code.20quality.3A.20simpa/with/594729278

depends on: [Merged by Bors] - feat(Tactic): add syntax for convert!, convert_to!, ac_change! #39715
depends on: [Merged by Bors] - feat(Tactic): automatically replace convert with convert! #39721
depends on: upcoming PRs that break this change into smaller chunks

github-actions · 2026-05-07T15:08:09Z

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

grunweg · 2026-05-07T15:11:08Z

How difficult is it to replace convert! by convert when the latter works?

Vierkantor · 2026-05-07T15:42:12Z

I'm working on it right now! (My idea was it pops up a Try this: convert message, so we can use Skimmer for auto-applying the changes.) It's not going to be completely trivial, since convert generally does not fail, just leaves more goals. So we have to run the two tactics in parallel and compare if the created goals are equivalent.

Vierkantor · 2026-05-07T17:48:08Z

I need to have dinner now, and it's going to be a busy weekend. If you'd like to push fixes, please go ahead! Otherwise I'll go and add a few more fixes in my unoccupied hours.

JovanGerb · 2026-05-09T23:09:20Z

Just to note, I had started another PR changing a setting in convert to make it more predictable and unfold less stuff (#38071), and there I also wanted to add a convert! for backward compatability.

I think that could fit together with the change in this PR by keeping convert! as the old behaviour in both aspects.

Vierkantor · 2026-05-13T09:42:39Z

I like the setting change in #38071!

Since this PR causes quite a bit of downstream breakage in congr! I think the right way to go now is to only change convert(!) and preserve the old behaviour in congr! for now. I'll copy @JovanGerb's approach of a custom Convert.Config structure with different defaults, which should make it easy to integrate the two PRs, hopefully.

github-actions · 2026-05-13T10:34:18Z

PR summary 5a6a0455e2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Convert.Config
+ Hom.toRationalMap
+ Opens.isDominant_homOfLE
+ Opens.isDominant_ι
+ PartialMap
+ PartialMap.IsOver
+ PartialMap.exists_restrict_isOver
+ PartialMap.isOver_toRationalMap_iff_of_isSeparated
+ PartialMap.le_domain_toRationalMap
+ PartialMap.restrict_toRationalMap
+ PartialMap.toPartialMap_toRationalMap_restrict
+ PartialMap.toRationalMap
+ PartialMap.toRationalMap_eq_iff
+ PartialMap.toRationalMap_surjective
+ RationalMap
+ RationalMap.IsOver
+ RationalMap.compHom
+ RationalMap.compHom_toRationalMap
+ RationalMap.dense_domain
+ RationalMap.domain
+ RationalMap.eq_of_fromFunctionField_eq
+ RationalMap.equivFunctionField
+ RationalMap.equivFunctionFieldOver
+ RationalMap.exists_partialMap_over
+ RationalMap.exists_rep
+ RationalMap.fromFunctionField
+ RationalMap.fromFunctionField_ofFunctionField
+ RationalMap.fromFunctionField_toRationalMap
+ RationalMap.isOver_iff
+ RationalMap.mem_domain
+ RationalMap.ofFunctionField
+ RationalMap.openCoverDomain
+ RationalMap.toPartialMap
+ RationalMap.toRationalMap_toPartialMap
+ _root_.AlgebraicGeometry.Scheme.Hom.toPartialMap
+ compHom
+ convexComboPair_same
+ dist_convexCombination_map_le
+ equiv
+ equiv_iff_of_domain_eq_of_isSeparated
+ equiv_iff_of_isSeparated
+ equiv_iff_of_isSeparated_of_le
+ equiv_of_fromSpecStalkOfMem_eq
+ equiv_toPartialMap_iff_of_isSeparated
+ equivalence_rel
+ ext
+ ext_iff
+ fromFunctionField
+ fromFunctionField_restrict
+ fromSpecStalkOfMem
+ fromSpecStalkOfMem_compHom
+ fromSpecStalkOfMem_ofFromSpecStalk
+ fromSpecStalkOfMem_restrict
+ fromSpecStalkOfMem_toPartialMap
+ instance : Setoid (X.PartialMap Y) := ⟨@PartialMap.equiv X Y, equivalence_rel⟩
+ instance [IsReduced X] [Y.IsSeparated] [S.IsSeparated] [X.Over S] [Y.Over S]
+ instance [X.Over S] [Y.Over S] (f : X ⟶ Y) [f.IsOver S] : f.toPartialMap.IsOver S
+ instance [X.Over S] [Y.Over S] (f : X.PartialMap Y) [f.IsOver S]
+ instance [X.Over S] [Y.Over S] (f : X.PartialMap Y) [f.IsOver S] : f.toRationalMap.IsOver S
+ instance [X.Over S] [Y.Over S] [Z.Over S] (f : X ⤏ Y) (g : Y ⟶ Z)
+ instance [X.Over S] [Y.Over S] [Z.Over S] (f : X.PartialMap Y) (g : Y ⟶ Z)
+ isOver_iff
+ isOver_iff_eq_restrict
+ mem_domain_ofFromSpecStalk
+ ofFromSpecStalk
+ ofFromSpecStalk_comp
+ p
+ restrict
+ restrict_equiv
+ restrict_id
+ restrict_id_hom
+ restrict_restrict
+ restrict_restrict_hom
+ semireducibleId
- IsCompact.tendsto_nhdsSet_of_mapClusterPt
- convexCombPair_same
- dist_iConvexComb_le

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

Vierkantor · 2026-05-13T16:43:19Z

Assuming build passes and we don't pick up more merge conflicts, I'm more or less happy with this PR. (There is the issue of some "Try this:" suggestions being slightly misformatted, which I would prefer to wait for the autoformatter.)

Let's think about how to get this merged without causing approximately a thousand merge conflicts. In the Zulip thread I have an idea for how to do so incrementally, what do you think?

mathlib-merge-conflicts · 2026-05-14T01:15:25Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-05-15T15:02:39Z

This pull request has conflicts, please merge master and resolve them.

joneugster · 2026-05-20T18:48:45Z

@maintainer: this is the relevant part of the change

joneugster · 2026-05-20T18:48:51Z

@maintainer: this is the relevant part of the change

joneugster · 2026-05-20T18:55:39Z

+  convert
+    ((H.comp hF).comp (mvPolynomialHomeomorph _ R A).isEmbedding).comp
+      (isEmbedding_precomp_of_surjective (R := R) fBC hfBC)


Suggested change

convert

((H.comp hF).comp (mvPolynomialHomeomorph _ R A).isEmbedding).comp

(isEmbedding_precomp_of_surjective (R := R) fBC hfBC)

convert ((H.comp hF).comp (mvPolynomialHomeomorph _ R A).isEmbedding).comp

(isEmbedding_precomp_of_surjective (R := R) fBC hfBC)

There is quite a few of these formatting changes without content. I assume they came from a script adding convert! first and then removing ! again? Maybe it be better to undo these formatting changes?

(on the other hand, since we don't yet have an auto-formatter in use, I won't insist on reverting these formatting changes)

joneugster · 2026-05-20T18:58:26Z

+    p.degrees = p.support.sup fun s : σ →₀ ℕ => Finsupp.toMultiset s := by rw [degrees]; convert
+      rfl


Suggested change

p.degrees = p.support.sup fun s : σ →₀ ℕ => Finsupp.toMultiset s := by rw [degrees]; convert

rfl

p.degrees = p.support.sup fun s : σ →₀ ℕ => Finsupp.toMultiset s := by

rw [degrees]

convert rfl

if reformatted, then better without ; which the style guide (weakly) prefers.

joneugster · 2026-05-20T19:05:43Z

@@ -274,8 +336,13 @@ example (a b c d e f g N : ℕ) : (a + b) + (c + d) + (e + f) + g ≤ N := by
 ```
 -/
 syntax (name := acChange) "ac_change " term (" using " num)? : tactic
+@[tactic_alt acChange]


Suggested change

@[tactic_alt acChange]

@[tactic_alt acChange]

joneugster · 2026-05-20T21:01:12Z

+        -- TODO: also enable this in the future? (Not right now, for backwards compatibility).
+        -- transparency := default,
+        -- preTransparency := default,
+        postTransparency := default }


does that mean there is no way to override this using the config and when postTransparency explicitly it will just be ignored?

It's a bit odd to me that you can write convert! (postTransparency := .reducible) ... or convert! (postTransparency := .default) ... and they do the same thing as the argument is overwritten.

But I guess I don't have a better solution either.

In #39928, I've come up with a solution involving two structure declarations with different default field values and their own declare_config_elab that we choose between.

joneugster · 2026-05-20T21:08:02Z

+    if semireducible.isSome then
+      liftMetaTactic fun g ↦ do
+        -- Suggest `convert` instead of `convert!` if that gives us the same goals.
+        let redGoals ← g.convert e sym.isSome (n.map (·.getNat)) baseConfig patterns
+        let defaultGoals ← g.convert e sym.isSome (n.map (·.getNat)) config patterns
+        if redGoals.length == defaultGoals.length then
+          let sameGoals ← try
+            (redGoals.zip defaultGoals).allM fun (g₁, g₂) => do
+              -- Check that they agree on the set of free variables, otherwise we get errors.
+              -- We assume the context in the `convert` case is a subset of the `convert!` case
+              -- since `convert!` can more agressively unfold and introduce more variables.
+              if !(← g₁.getDecl).lctx.isSubPrefixOf (← g₂.getDecl).lctx then return false
+              g₂.withContext <| withReducible <| isDefEq (← g₁.getType) (← g₂.getType)
+            catch _ => pure false
+          if sameGoals then
+            let tac ← `(tactic| convert%$tk $cfg $[←%$sym]? $term $[using $n]? $[with $ps?*]?)
+            TryThis.addSuggestion tk { suggestion := tac } (origSpan? := ← getRef)
+        return defaultGoals ++ gs
+    else
+      liftMetaTactic fun g ↦
+        return (← g.convert e sym.isSome (n.map (·.getNat)) config patterns) ++ gs


I assume this was here for you to figure out which ! to remove for this PR. Is your intent to keep this in for the final PR? Isn't that quite inefficient?

This is indeed inefficient, but I don't know a good way to add the "Try this:" otherwise. I figure it might make a nice lint, perhaps hidden behind an off-by-default option? We could benchmark it in the final version.

joneugster · 2026-05-20T21:09:38Z

+        -- TODO: also enable this in the future? (Not right now, for backwards compatibility).
+        -- transparency := default,
+        -- preTransparency := default,
+        postTransparency := default }


(same question as above)

joneugster · 2026-05-20T21:28:05Z

    $[with $ps?*]? $[$loc?:location]?) => do
  let n : ℕ := n |>.map (·.getNat) |>.getD 1
-  let config ← Congr!.elabConfig (mkOptionalNode cfg)
+    let mut config := { ← Convert.elabConfig cfg with }


wrong indent?

This PR prepares for #39039 by adding the required syntax. Once this PR is in, we'll do a global find and replace for changing `convert` to `convert!` (without changing the behaviour), and finally we will enable the new behaviour for `convert`.

…39715) This PR prepares for #39039 by adding the required syntax. Once this PR is in, we'll do a global find and replace for changing `convert` to `convert!` (without changing the behaviour), and finally we will enable the new behaviour for `convert`. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

Otherwise it turns out some proofs break.

…vert`

mathlib-dependent-issues · 2026-05-23T10:48:54Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Tactic): add syntax for convert!, convert_to!, ac_change! #39715~~
~~[Merged by Bors] - feat(Tactic): automatically replace convert with convert! #39721~~
By Dependent Issues (🤖). Happy coding!

…eanprover-community#39715) This PR prepares for leanprover-community#39039 by adding the required syntax. Once this PR is in, we'll do a global find and replace for changing `convert` to `convert!` (without changing the behaviour), and finally we will enable the new behaviour for `convert`. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

…-community#39721) This PR makes any use of `convert` pop up a "Try this:" message replacing it with `convert!`. This prepares for leanprover-community#39039 which will make `convert` change behaviour and `convert!` retain the old behaviour. Note that `convert` and `convert!` still do the same thing and result in the same goals after this PR is applied, except `convert!` does not pop up a "Try this:" afterwards. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

mathlib-merge-conflicts · 2026-05-26T03:54:35Z

This pull request has conflicts, please merge master and resolve them.

JovanGerb · 2026-05-26T17:21:29Z

Now that all uses of convert have been changed to convert!, will we do the same for convert_to!?

Also, what do you think about congr!? Its name has an !, so it seems reasonable that it aggressively reduces. The problem is that the name congr is already takes by a tactic in core. Should we just override congr? I can't think of many uses of the current congr tactic.

By the way, my other PR changing the behaviour of convert is about the following that I don't think convert should be doing:

example (f g : Nat → Prop) (a b : Nat) (h : f a) : g b := by
  convert h
  -- ⊢ g = f
  -- ⊢ b = a

It should only do congruence steps when the head function on both sides is the same. I'll wait with working on that PR until this one is merged to avoid merge conflicts.

Vierkantor · 2026-05-26T20:02:39Z

(Quick answer for this sentence, I'll write a full response when I am ready tomorrow.)

I'll wait with working on that PR until this one is merged to avoid merge conflicts.

My plan is to get a PR ready which updates convert's behaviour but doesn't replace any usages yet (except in MathlibTest). This should be compatible with your PR. And then when both changes are in we can do the replacement from convert! to convert without having to do any manual fixes (I hope!).

…eanprover-community#39715) This PR prepares for leanprover-community#39039 by adding the required syntax. Once this PR is in, we'll do a global find and replace for changing `convert` to `convert!` (without changing the behaviour), and finally we will enable the new behaviour for `convert`. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

…-community#39721) This PR makes any use of `convert` pop up a "Try this:" message replacing it with `convert!`. This prepares for leanprover-community#39039 which will make `convert` change behaviour and `convert!` retain the old behaviour. Note that `convert` and `convert!` still do the same thing and result in the same goals after this PR is applied, except `convert!` does not pop up a "Try this:" afterwards. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

…eanprover-community#39715) This PR prepares for leanprover-community#39039 by adding the required syntax. Once this PR is in, we'll do a global find and replace for changing `convert` to `convert!` (without changing the behaviour), and finally we will enable the new behaviour for `convert`. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

…-community#39721) This PR makes any use of `convert` pop up a "Try this:" message replacing it with `convert!`. This prepares for leanprover-community#39039 which will make `convert` change behaviour and `convert!` retain the old behaviour. Note that `convert` and `convert!` still do the same thing and result in the same goals after this PR is applied, except `convert!` does not pop up a "Try this:" afterwards. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

This PR implements the main behaviour change from #39039: `convert` now discharges side goals at reducible transparency. `convert!`, which we previously switched all calls inside Mathlib to, keeps the old behaviour of working at default transparency. (Everything discussed in this PR holds analogously for the other tactics in the family: `convert_to` and `ac_change`). The main trick in this PR is in allowing `convert!` to have different configuration options than `convert`, but still allow the user to override those options too. So `convert! (postTransparency := .instances)` will have transparency set to `.instances`, not `.default`. We achieve this by having two new structures that copy `Congr!.Config` but set different default values, and choosing between the corresponding elaborators for those configs based on the presence of an `!`. I got this trick from Jovan's #38071 which also changes settings in `Convert.Config`. This PR should be mostly compatible with #38071 and I'd like to get both this one and #38071 in before wrapping up #39039 by replacing unnecessary calls to `convert!` with `convert`.

This PR implements the main behaviour change from #39039: `convert` now discharges side goals at reducible transparency. `convert!`, which we previously switched all calls inside Mathlib to, keeps the old behaviour of working at default transparency. (Everything discussed in this PR holds analogously for the other tactics in the family: `convert_to` and `ac_change`). The main trick in this PR is in allowing `convert!` to have different configuration options than `convert`, but still allow the user to override those options too. So `convert! (postTransparency := .instances)` will have transparency set to `.instances`, not `.default`. We achieve this by having two new structures that copy `Congr!.Config` but set different default values, and choosing between the corresponding elaborators for those configs based on the presence of an `!`. I got this trick from Jovan's #38071 which also changes settings in `Convert.Config`. This PR should be mostly compatible with #38071 and I'd like to get both this one and #38071 in before wrapping up #39039 by replacing unnecessary calls to `convert!` with `convert`. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

…ommunity#39928) This PR implements the main behaviour change from leanprover-community#39039: `convert` now discharges side goals at reducible transparency. `convert!`, which we previously switched all calls inside Mathlib to, keeps the old behaviour of working at default transparency. (Everything discussed in this PR holds analogously for the other tactics in the family: `convert_to` and `ac_change`). The main trick in this PR is in allowing `convert!` to have different configuration options than `convert`, but still allow the user to override those options too. So `convert! (postTransparency := .instances)` will have transparency set to `.instances`, not `.default`. We achieve this by having two new structures that copy `Congr!.Config` but set different default values, and choosing between the corresponding elaborators for those configs based on the presence of an `!`. I got this trick from Jovan's leanprover-community#38071 which also changes settings in `Convert.Config`. This PR should be mostly compatible with leanprover-community#38071 and I'd like to get both this one and leanprover-community#38071 in before wrapping up leanprover-community#39039 by replacing unnecessary calls to `convert!` with `convert`. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

Vierkantor added the t-meta Tactics, attributes or user commands label May 7, 2026

github-actions Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 7, 2026

Vierkantor added the WIP Work in progress label May 7, 2026

Vierkantor changed the title ~~feat(Tactic): congr! and convert now discharge side goals at reducible transparency~~ feat(Tactic): congr! and convert now discharge side goals at reducible transparency May 7, 2026

Vierkantor mentioned this pull request May 13, 2026

[Merged by Bors] - feat(Convert): less aggressive congruence #38071

Closed

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 13, 2026

github-actions Bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels May 13, 2026

Vierkantor removed the WIP Work in progress label May 13, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 14, 2026

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 14, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 15, 2026

joneugster reviewed May 20, 2026

View reviewed changes

joneugster self-assigned this May 20, 2026

joneugster added the awaiting-author A reviewer has asked the author a question or requested changes. label May 20, 2026

Vierkantor mentioned this pull request May 22, 2026

[Merged by Bors] - feat(Tactic): add syntax for convert!, convert_to!, ac_change! #39715

Closed

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 22, 2026

Vierkantor added 8 commits May 23, 2026 11:07

Fixes.

07958e5

(Temporarily?) only set postTransparency := default

2519dba

Otherwise it turns out some proofs break.

As much fixes as I can get in before dinnertime.

02e1716

Stay with default reducibility in congr! and only change it in `con…

66ddb61

…vert`

Fix: also elaborate config correctly in presence of ! in convert_to

36fc918

Fixes

5e24e12

Add tactic alt tags.

d696472

Missing docstring

2763d79

Vierkantor force-pushed the reducible-convert branch from afb33db to 2763d79 Compare May 23, 2026 10:13

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 23, 2026

Vierkantor and others added 2 commits May 23, 2026 11:14

Use Skimmer to remove all the unnecessary convert!s

47f1b90

[pre-commit.ci lite] apply automatic fixes

5a6a045

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 23, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 26, 2026

Vierkantor changed the title ~~feat(Tactic): congr! and convert now discharge side goals at reducible transparency~~ feat(Tactic): convert now discharges side goals at reducible transparency May 27, 2026

Vierkantor added the WIP Work in progress label May 27, 2026

Vierkantor mentioned this pull request May 27, 2026

[Merged by Bors] - feat(Tactic): convert discharges side goals reducibly #39928

Closed

		p.degrees = p.support.sup fun s : σ →₀ ℕ => Finsupp.toMultiset s := by rw [degrees]; convert
		rfl

Uh oh!

Conversation

Vierkantor commented May 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

✅ PR Title Formatted Correctly

Uh oh!

grunweg commented May 7, 2026

Uh oh!

Vierkantor commented May 7, 2026

Uh oh!

Vierkantor commented May 7, 2026

Uh oh!

JovanGerb commented May 9, 2026

Uh oh!

Vierkantor commented May 13, 2026

Uh oh!

github-actions Bot commented May 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5a6a0455e2

Import changes for modified files

Declarations diff

Uh oh!

Vierkantor commented May 13, 2026

Uh oh!

mathlib-merge-conflicts Bot commented May 14, 2026

Uh oh!

mathlib-merge-conflicts Bot commented May 15, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mathlib-dependent-issues Bot commented May 23, 2026

Uh oh!

mathlib-merge-conflicts Bot commented May 26, 2026

Uh oh!

JovanGerb commented May 26, 2026

Uh oh!

Vierkantor commented May 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Vierkantor commented May 7, 2026 •

edited

Loading

github-actions Bot commented May 7, 2026 •

edited

Loading

github-actions Bot commented May 13, 2026 •

edited

Loading