perf(FieldTheory/PurelyInseparable): golf proof

[kbuzzard]

This one proof was taking a huge amount of time to typecheck, presumably because of some defeq abuse. Fixing this up gives a nice speedup in this file.

---

Claude says: The old proof transported Algebra.IsSeparable M L across the definitional equality between (inclusion hi).toAlgebra and the canonical Algebra instance on extendScalars hi. Checking that single instance defeq costs the kernel ~460ms (~80% of the file's kernel type-checking time), and it is paid twice if the haveI there is replaced by have (the cause of the 13.6% instruction-count regression radar reported on #41615).

What Claude says looks reasonable to me.

[kbuzzard]

!radar

[leanprover-radar]

Benchmark results for 23363c2 against 4694604 are in. No significant results found. @kbuzzard

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run main differ between commits.

• ✅ build//instructions: -187.7G (-0.12%)

Medium changes (1✅)

• ✅ build/module/Mathlib.FieldTheory.PurelyInseparable.PerfectClosure//instructions: -6.6G (-20.55%)

Small changes (1✅)

1 hidden

[github-actions]

PR summary 23363c2bd3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

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)

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

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 23363c2bd3
Reference commit 4694604756

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.sh 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).

[kbuzzard]

I think the 187G figure must be bogus but the 20% speedup in the file I'm editing is genuine.

[acmepjz]

Suggested change

	· have : Algebra.IsSeparable M (adjoin M {x}) :=
	· have : Algebra.IsSeparable M M⟮x⟯ :=

Maybe this looks better (untested) Same as two adjoin M {x} below.

[jcommelin]

bors d+

[mathlib-bors]

✌️ kbuzzard can now approve this pull request until 2026-07-27 09:36 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.