chore: downstream-lean4 adaptations for nightly-2026-10-21 by downstream-lean4[bot] · Pull Request #45142 · leanprover-community/mathlib4

downstream-lean4 · 2026-10-21T18:48:35Z

This PR contains automatically exported adaptations up until leanprover/downstream-lean4@8fdad89.

If any dependencies have open export PRs themselves, you may need to merge them first and then run lake update in this PR. If this PR becomes outdated, just close it and a new one will be opened soon. No new export PRs will be opened while one is already open.

downstream-sha: 8fdad89b8cbf3659ca3427c419f0a5b982b7a0c5

github-actions · 2026-10-21T18:48:46Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to Zulip and join the Lean community.
Thank you again for joining our community.

github-actions · 2026-10-21T18:49:48Z

PR summary 8bc0022b90

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

- dthen
- dthen_eq_then

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.

Declarations diff (Lean -- stale, waiting for the new build)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 8fe54d9).

+1 new declarations
−2 removed declarations

+CategoryTheory.ConcreteCategory.hom.hcongr_9
-Ordering.dthen
-Ordering.dthen_eq_then

Increase in strong tech debt: (relative, absolute) = (1.77, 0.23)

Current number	Change	Type (strong)
391	5	adaptation notes
26	1	disabled simpNF lints
11	2	disabled deprecation lints

No changes to weak technical debt.

Current commit 8bc0022b90
Reference commit d88814353f

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Vierkantor · 2026-10-22T12:50:27Z

-    simp only [Equiv.toFun_as_coe, Equiv.prodCongr_apply, EquivLike.coe_coe,
-      Prod.map, map_mul, Prod.mk_mul_mk]
+    simp only [Equiv.toFun_as_coe, Equiv.prodCongr_apply, Prod.map, EquivLike.coe_coe, map_mul,
+      Prod.mk_mul_mk]


I don't think we should merge these changes, since the two versions do the same thing and will just cause merge conflicts down the line.

Vierkantor

I need to run for a bit, but when I come back I plan to revert a lot of these changes since they appear unnecessary.

Vierkantor · 2026-10-22T12:53:20Z

+    rw [AlgHom.comp_apply,
+      map_eq_zero_iff _ (rename_injective _ (fun _ _ _ ↦ rfl (α := PUnit.{u + 1})))] at this


This change seems to be unnecessary too.

Vierkantor · 2026-10-22T12:53:48Z

-theorem continuous_re : Continuous fun q : ℍ => q.re :=
-  (PiLp.continuous_apply 2 _ 0).comp linearIsometryEquivTuple.continuous
+theorem continuous_re : Continuous fun q : ℍ => q.re := by
+  convert! (PiLp.continuous_apply 2 _ 0).comp linearIsometryEquivTuple.continuous


Also seems to be unnecessary...

Vierkantor · 2026-10-22T12:54:08Z

  let ⟨_,b,_⟩ := f
  let ⟨_,e,_⟩ := g
  congr
-  simp only [eq_iff_true_of_subsingleton]


This is indeed a positive change!

Vierkantor · 2026-10-22T12:56:44Z

 def commMonToLaxBraidedObj (A : CommMon C) :
    Discrete PUnit.{u + 1} ⥤ C := (Functor.const _).obj A.X

+attribute [nolint simpNF] commMonToLaxBraidedObj_map


This needs an adaptation note at least. We might even get away with removing the lemma altogether since both versions reduce to "this map is the identity":

@[simps! obj] -- `map` can already be proven. def commMonToLaxBraidedObj (A : CommMon C) : Discrete PUnit.{u + 1} ⥤ C := (Functor.const _).obj A.X

Vierkantor · 2026-10-22T12:57:07Z

+attribute [nolint simpNF] equivLaxMonoidalFunctorPUnit_inverse_obj_map
+AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_map


Suggested change

attribute [nolint simpNF] equivLaxMonoidalFunctorPUnit_inverse_obj_map

AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_map

attribute [nolint simpNF] equivLaxMonoidalFunctorPUnit_inverse_obj_map

AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_map

Vierkantor · 2026-10-22T12:58:57Z

            (trNat_natEnd _) ⟨rfl, by simp⟩))
        (TransGen.head rfl (TransGen.head rfl ?_))
    simp only [TM2.step, Option.mem_def, trList, List.append_assoc,
-      List.cons_append, elim_update_stack, elim_rev, elim_update_rev, Function.update_self,


Vierkantor · 2026-10-22T12:59:28Z

+    · simp only [Nat.one_mod, Nat.mod_add_mod]
+      rw [← Nat.mod_eq_of_lt h, Nat.mod_mod]
    · rw [Fin.val_mk, not_lt] at h
-      simp only [Nat.mod_add_mod,


Vierkantor · 2026-10-22T13:00:01Z

    rw [← MonoidHom.mem_range, S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv,
      rightHom_splitting, mul_inv_cancel]
  map_mul' := fun ⟨n₁, g₁⟩ ⟨n₂, g₂⟩ ↦ by
-    simp only [conjAct, MonoidHom.comp_apply, map_mul, inl_conjAct_comm, MonoidHom.coe_ofClass]


Vierkantor · 2026-10-22T13:00:46Z

  simp only [funMap_quotient_mk', Quotient.eq]
  obtain ⟨k, ik, jk⟩ :=
    directed_of (· ≤ ·) i (Classical.choose (Finite.bddAbove_range fun _ : Fin n => i))
-  refine ⟨k, jk, ik, ?_⟩


Vierkantor · 2026-10-22T13:01:01Z

  right_inv := by
    rintro ⟨m, hm₀, hm⟩
-    rw [Subtype.mk.injEq, ← primeFactorsList_count_eq, ← prod_replicate, ← prod_append]
+    simp_rw [Subtype.mk.injEq, ← primeFactorsList_count_eq, ← prod_replicate, ← prod_append]


downstream-sha: 9b8dac4990f3ae8539a2b30942a7afc37f8a118f

Garmelon · 2026-10-26T18:13:46Z

Closing this PR so it is recreated by downstream-lean4. @Vierkantor I'm not sure if all your review comments were covered by the fixes you pushed to downstream-lean4, so you may want to keep this PR in mind when reviewing the next one.

Garmelon · 2026-10-26T19:37:41Z

The new PR is at #45327

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Oct 21, 2026

github-actions Bot added the increases-technical-debt Automatically added label for PRs which increase "strong" technical debts label Oct 21, 2026

downstream-lean4 Bot force-pushed the downstream-lean4-export branch from 18c3e78 to e08fc13 Compare October 21, 2026 22:47

kim-em mentioned this pull request Oct 22, 2026

fix: find existing PRs from a fork with the same owner leanprover/downstream#7

Open

downstream-lean4 Bot force-pushed the downstream-lean4-export branch 3 times, most recently from d542bba to 8fe54d9 Compare October 22, 2026 11:17

Vierkantor reviewed Oct 22, 2026

View reviewed changes

Vierkantor requested changes Oct 22, 2026

View reviewed changes

Vierkantor added the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Oct 22, 2026

downstream-lean4 Bot force-pushed the downstream-lean4-export branch 5 times, most recently from 44646e6 to 470fa82 Compare October 25, 2026 11:14

chore: downstream-lean4 adaptations for nightly-2026-10-25

8bc0022

downstream-sha: 9b8dac4990f3ae8539a2b30942a7afc37f8a118f

downstream-lean4 Bot force-pushed the downstream-lean4-export branch from 470fa82 to 8bc0022 Compare October 26, 2026 10:13

Garmelon closed this Oct 26, 2026

		rw [AlgHom.comp_apply,
		map_eq_zero_iff _ (rename_injective _ (fun _ _ _ ↦ rfl (α := PUnit.{u + 1})))] at this

		attribute [nolint simpNF] equivLaxMonoidalFunctorPUnit_inverse_obj_map
		AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_map

Conversation

downstream-lean4 Bot commented Oct 21, 2026

Uh oh!

github-actions Bot commented Oct 21, 2026

Welcome new contributor!

Uh oh!

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

Uh oh!

PR summary 8bc0022b90

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean -- stale, waiting for the new build)

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Vierkantor left a comment

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!

Choose a reason for hiding this comment

Uh oh!

Garmelon commented Oct 26, 2026

Uh oh!

Garmelon commented Oct 26, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions Bot commented Oct 21, 2026 •

edited

Loading