This PR leverages the fact that expressions are type correct in
`grind` and the conclusion of extensionality theorems is of the form
`?a = ?b`.

This PR is relevant for #12179 because it enables us to use a weaker
`isDefEq` that does not bump the transparency level when processing
implicit arguments.

This PR leverages the fact that expressions are type correct in `grind`
and the conclusion of extensionality theorems is of the form `?a = ?b`.

This PR is relevant for #12179 because it enables us to use a weaker
`isDefEq` that does not bump the transparency level when processing
implicit arguments.

This PR implements preparatory work for #12179. It implements a new
feature in `isDefEq` to ensure it does not increase the transparency
level to `.default` when checking definitionally equality of implicit
arguments. This transparency level bump was introduced in Lean 3, but it
is not a performance issue and is affecting Mathlib. This PR adds the
new feature, but it is disabled by default.

This PR fixes a gap in how `@[implicit_reducible]` is assigned to parent
projections during structure elaboration.

When `class C extends P₁, P₂` has diamond inheritance, some ancestor
structures become constructor subobject fields even though they aren't
direct parents. For example, in `Monoid extends Semigroup, MulOneClass`,
`One` becomes a constructor subobject of `Monoid` — its field `one`
doesn't overlap with `Semigroup`'s fields, and `inSubobject?` is `none`
during `MulOneClass` flattening.

`mkProjections` creates the projection `Monoid.toOne` but defers
reducibility to `addParentInstances` (guarded by `if !instImplicit`).
However, `addParentInstances` only processes direct parents from the
`extends` clause. Grandparent subobject projections fall through the gap
and stay `semireducible`.

This causes defeq failures when `backward.isDefEq.respectTransparency`
is enabled (#12179): at `.instances` transparency, the semireducible
grandparent projection can't unfold, so two paths to the same ancestor
structure aren't recognized as definitionally equal.

Fix: before `addParentInstances`, iterate over all `.subobject` fields
and set `implicitReducible` on those whose parent is a class.

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.6 <[email protected]>

* revert changes to GCongr

* fix tests output again

* fix

* maxheartbeats

* fix

* chore: bump to nightly-2026-02-12

* merge lean-pr-testing-12412

* bump toolchain (early today, oops!)

* fix lakefile and lake update

* remove upstreamed

* restore a simp

* remove upstreamed and deprecation

* deprecation

* clarify adaptation note

* lake update

* fix for leanprover/lean4#11744

* fix indentation

* chore: bump to nightly-2026-02-13-rev1

* chore: bump to nightly-2026-02-13-rev2

* fix test

* fix test

* nice, most workarounds not needed with univ_out_params

* chore: bump to nightly-2026-02-14

* chore: update batteries for List.reverse_singleton fix

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* .

* add @[univ_out_params] where universe params are not determined by inputs

Classes like `Category.{v}`, `HasLimitsOfSize.{v₁,u₁}`, `Functor.IsContinuous.{t}`,
and `UCompactlyGeneratedSpace.{u}` have universe parameters that do not appear in
their input parameter types. With the new TC resolution cache (lean4#12286), these
default to output parameters, causing cache collisions when the same class is queried
at different universe levels.

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* add #adaptation_note for @[univ_out_params] annotations

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* add library note on universe output parameters, update adaptation notes

Adds a library note in Category/Basic.lean explaining how `@[univ_out_params]`
interacts with the TC resolution cache, with concrete examples of when universe
parameters should and should not be treated as outputs.

Updates all adaptation notes to use a shorter form referencing this library note.

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* convert #adaptation_note to -- comments for univ_out_params annotations

These are permanent annotations, not temporary workarounds, so
#adaptation_note is the wrong mechanism. Use regular comments placed
after the doc-string and before the @[univ_out_params] attribute.

Also restore the reference to lean4#12423 alongside lean4#12286.

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* fix

* fix

* fix

* fix

* empty commit to retrigger CI

* chore: bump to nightly-2026-02-15

* lake update

* chore: bump to nightly-2026-02-15-rev1

* lake update

* chore: bump to nightly-2026-02-16

* Update lean-toolchain for leanprover/lean4#12179

* fix_backward_defeq script

* lake update batteries

* non-local set_option, added manually

* manual fixes, script confused by absence of blank lines

* times out without manual fix

* norm_num tests

* reduce_mod_char

* fix test output

* set_option globally in RingTheory.SimpleModule.Isotypic

* set_option globally in RingTheory.Adjoin.Dimension

* set_option a section of LinearAlgebra.FiniteDimensional.Basic

* set_option globally in Algebra.Homology.BifunctorAssociator

* set_option in section in Algebra.Homology.BifunctorHomotopy

* set_option globally in Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

* set_option globally in Algebra.Homology.BifunctorShift

* set_option in section in Geometry.Manifold.Riemannian.Basic

* set_option in section in NumberTheoryCyclotomic.Basic

* set_option in section in Analysis.Distribution.SchwartzSpace.Fourier

* global set_option in RingTheory.DedekindDomain.LinearDisjoint

* manual fixes for CategoryTheory.Monoidal.DayConvolution.Closed

* manual fixes for CategoryTheory.Sites.Descent.IsStack

* manual fixes for Algebra.Homology.DifferentialObject

* manual fixes for Geometry.RingedSpace.PresheafedSpace

* manual fixes for CategoryTheory.Triangulated.Opposite.Functor

* manual fixes in Algebra.Homology.HomotopyCategory.ShortExact

* manual fixes for Geometry.RingedSpace.PresheafedSpace.Gluing

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* manual fixes to CategoryTheory.Sites.Descent.DescentData

* manual fixes, script confused by absence of blank lines, and a module-doc that should have been a doc-string

* adaptation_note

* x: ./fix_backward_defeq.py

* x: ./fix_backward_defeq.py

* set_option linter.style.longFile

* remove unused simp args

* remove noop tactic

* lake update

* optimistic linter fixes

* patch and adaptation note

* slightly more care with the linter

* still getting it right

* fix test

* chore: adaptations for nightly-2026-02-15-rev1 (#177)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Ruben Van de Velde <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>

* fix warning

* fix

* fix properly

* chore: adaptations for nightly-2026-02-16 (#179)



Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>

* Merge master into nightly-testing

* chore: bump to nightly-2026-02-16-rev1

* move batteries back to nightly-testing

* lake update

* final fixes for leanprover/lean4#1279

* fix for leanprover/lean4#12179

* fix for leanprover/lean4#12179

* fix for leanprover/lean4#12179

* fix for leanprover/lean4#12179

* fix for leanprover/lean4#12179

* fix for leanprover/lean4#12179

* chore: adaptations for nightly-2026-02-16-rev1 (#180)

* fix_backward_defeq script

* lake update batteries

* non-local set_option, added manually

* manual fixes, script confused by absence of blank lines

* times out without manual fix

* norm_num tests

* reduce_mod_char

* fix test output

* set_option globally in RingTheory.SimpleModule.Isotypic

* set_option globally in RingTheory.Adjoin.Dimension

* set_option a section of LinearAlgebra.FiniteDimensional.Basic

* set_option globally in Algebra.Homology.BifunctorAssociator

* set_option in section in Algebra.Homology.BifunctorHomotopy

* set_option globally in Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

* set_option globally in Algebra.Homology.BifunctorShift

* set_option in section in Geometry.Manifold.Riemannian.Basic

* set_option in section in NumberTheoryCyclotomic.Basic

* set_option in section in Analysis.Distribution.SchwartzSpace.Fourier

* global set_option in RingTheory.DedekindDomain.LinearDisjoint

* manual fixes for CategoryTheory.Monoidal.DayConvolution.Closed

* manual fixes for CategoryTheory.Sites.Descent.IsStack

* manual fixes for Algebra.Homology.DifferentialObject

* manual fixes for Geometry.RingedSpace.PresheafedSpace

* manual fixes for CategoryTheory.Triangulated.Opposite.Functor

* manual fixes in Algebra.Homology.HomotopyCategory.ShortExact

* manual fixes for Geometry.RingedSpace.PresheafedSpace.Gluing

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* manual fixes to CategoryTheory.Sites.Descent.DescentData

* manual fixes, script confused by absence of blank lines, and a module-doc that should have been a doc-string

* adaptation_note

* x: ./fix_backward_defeq.py

* x: ./fix_backward_defeq.py

* set_option linter.style.longFile

* remove unused simp args

* remove noop tactic

* lake update

* optimistic linter fixes

* patch and adaptation note

* slightly more care with the linter

* still getting it right

* fix test

* chore: adaptations for nightly-2026-02-16-rev1

* fix lakefile and manifest

* remove fix_backward_defeq.py

---------

Co-authored-by: Claude Opus 4.6 <[email protected]>

* chore: bump to nightly-2026-02-17

* chore: remove fix_backward_defeq.py (no longer needed)

* Update lean-toolchain for testing leanprover/lean4#12538

* Update lean-toolchain for testing leanprover/lean4#12564

* fixes for leanprover/lean4#12564

* fixes for leanprover/lean4#12564

* fixes for leanprover/lean4#12564

* fixes for leanprover/lean4#12564

* fixes for leanprover/lean4#12564

* temporary sorries to get further through the build

* fixes for sorries

* more set_option

* blech

* more fixes

* cleanup

* remove 316 set_options

* fix Algebra.Category.ModuleCat.Differentials.Presheaf

* remove unnecessary set_option

* remove more set_option backward.isDefEq.respectTransparency false

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* chore: bump to nightly-2026-02-19

* chore: adaptations for nightly-2026-02-19

Rename instanceReducible to implicitReducible (lean4#12529).
Update batteries for upstreamed List.scanl/scanr (lean4#12452)
and Nat.Digits (lean4#12445).

* pre-emptively set toolchain

* fixes for leanprover/lean4#12572

* fixes for leanprover/lean4#12572

* Update lean-toolchain for leanprover/lean4#12572

* remove set_option

* remove set_option

* fixes for leanprover/lean4#12572

* fixes for leanprover/lean4#12572

* fixes for leanprover/lean4#12572

* fixes for leanprover/lean4#12538

* remove more

* fixes for leanprover/lean4#12538

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* fixes for leanprover/lean4#12538

* fixes for leanprover/lean4#12538

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* Update lean-toolchain for testing leanprover/lean4#12603

* chore: bump to nightly-2026-02-20

* fixes for leanprover/lean4#12538

* fixes

* Update lean-toolchain for testing leanprover/lean4#12625

* fix

* chore: adaptations for nightly-2026-02-20

* Merge master into nightly-testing

* fix

* chore: bump to nightly-2026-02-21

* chore: adaptations for nightly-2026-02-21

* Update lean-toolchain for leanprover/lean4#12625

* fix

* fixes

* fix

* Update lean-toolchain for leanprover/lean4#12538

* fixes

* fixes

* fixes

* chore: bump to nightly-2026-02-22

* fix cexample

* fix test

* Update lean-toolchain for leanprover/lean4#12625

* chore: adapt to mkHole type change from lean4#12459

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* chore: adaptations for nightly-2026-02-22

* lake update

* bump batteries

* fixes

* Update lean-toolchain for leanprover/lean4#12564

* set_option

* set_option

* set_option

* fix(Linter/TextBased): don't flag "see adaptation note" comments

The `adaptationNoteLinter` was matching any line containing the
substring "daptation note", which caused false positives on lines
like `set_option maxHeartbeats 400000 in -- see adaptation note`
that merely reference a nearby `#adaptation_note` command.

Exclude lines containing `#adaptation_note` (correct usage) and
lines containing `see adaptation note` (cross-references).

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* chore: bump to nightly-2026-02-23

* fixes

* adaptation notes

* fixes

* fixes

* fixes

* lint

* fix

* fix

* fix test

* fixes for leanprover/lean4#12650

* chore: adaptations for nightly-2026-02-23

* chore: bump to nightly-2026-02-23-rev1

* merge lean-pr-testing-12650

* chore: bump to nightly-2026-02-23-rev2

* x: scripts/add_set_option.py

* chore: bump to nightly-2026-02-25

* scripts/add_set_option.py

* fixes

* fixes

* fix

* fixes

* chore: bump to nightly-2026-02-25

* merge lean-pr-testing-12603

* bump batteries

* what happened there?

* lake update

* lake update aesop

* fixes

* chore: adaptations for nightly-2026-02-25

---------

Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Ruben Van de Velde <[email protected]>
Co-authored-by: Claude Opus 4.6 <[email protected]>
Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: Joël Riou <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Sebastian Graf <[email protected]>

This PR fixes a gap in how `@[implicit_reducible]` is assigned to parent
projections during structure elaboration.

When `class C extends P₁, P₂` has diamond inheritance, some ancestor
structures become constructor subobject fields even though they aren't
direct parents. For example, in `Monoid extends Semigroup, MulOneClass`,
`One` becomes a constructor subobject of `Monoid` — its field `one`
doesn't overlap with `Semigroup`'s fields, and `inSubobject?` is `none`
during `MulOneClass` flattening.

`mkProjections` creates the projection `Monoid.toOne` but defers
reducibility to `addParentInstances` (guarded by `if !instImplicit`).
However, `addParentInstances` only processes direct parents from the
`extends` clause. Grandparent subobject projections fall through the gap
and stay `semireducible`.

This causes defeq failures when `backward.isDefEq.respectTransparency`
is enabled (#12179): at `.instances` transparency, the semireducible
grandparent projection can't unfold, so two paths to the same ancestor
structure aren't recognized as definitionally equal.

Fix: before `addParentInstances`, iterate over all `.subobject` fields
and set `implicitReducible` on those whose parent is a class.

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.6 <[email protected]>