[Merged by Bors] - refactor(NumberTheory): golf Mathlib/NumberTheory/Cyclotomic/Gal

[yuanyi-350]

• simplifies autToPow_injective in Mathlib/NumberTheory/Cyclotomic/Gal by reusing IsPrimitiveRoot.autToPow_spec instead of expanding the proof through roots of unity and pow_eq_pow_iff_modEq
• keeps the proof structured as an algHom_ext argument on the power basis, but removes the intermediate bookkeeping lemmas and coercion manipulations

Extracted from #38144

[yuanyi-350]

!bench

[leanprover-radar]

Benchmark results for 8418eab against 9268b22 are in. No significant results found. @yuanyi-350

• 🟥 build//instructions: +4.2G (+0.00%)

Small changes (2🟥)

• 🟥 build/module/Mathlib.Data.Char//instructions: +124.6M (+5.27%)
• 🟥 build/module/Mathlib.MeasureTheory.MeasurableSpace.Card//instructions: +424.2M (+3.53%)

[github-actions]

PR summary 9268b22206

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

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

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

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

[yuanyi-350]

I ran a profiler comparison for the changed declarations in this PR.

Results (seconds):

• IsPrimitiveRoot.autToPow_injective: 0.117810 -> 0.032246 (-72.63%)

Overall:

• IsPrimitiveRoot.autToPow_injective elaborates substantially faster after the refactor.

[MichaelStollBayreuth]

LGTM
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by MichaelStollBayreuth.

[riccardobrasca]

Are you abusing defeq here?

[yuanyi-350]

@riccardobrasca , My bad, I definitely used the defeq between AlgEquiv and toAlgHom before! This new update should be standard, though. I'm really curious, how do you usually catch this sort of defeq abuse? Is it just intuition? I was wondering if we could try automating the defeq abuse detection process to help out the community better.

[yuanyi-350]

1. Mathlib/NumberTheory/Cyclotomic/Gal.lean:59

Code: apply AlgEquiv.coe_algHom_injective

Actual state transition in the proof:
Before:

⊢ f = g

After:

⊢ (f : L →ₐ[K] L) = (g : L →ₐ[K] L)

Designed state transition from the theorem type:

AlgHomClass.toAlgHom.Injective

2. Mathlib/NumberTheory/Cyclotomic/Gal.lean:60

Code: apply (hμ.powerBasis K).algHom_ext

Actual state transition in the proof:
Before:

⊢ (f : L →ₐ[K] L) = (g : L →ₐ[K] L)

After:

⊢ (f : L →ₐ[K] L) ((hμ.powerBasis K).gen : L) =
     (g : L →ₐ[K] L) ((hμ.powerBasis K).gen : L)

Designed state transition from the theorem type:

((f : L →ₐ[K] L) ((hμ.powerBasis K).gen : L) =
(g : L →ₐ[K] L) ((hμ.powerBasis K).gen : L)) →
(f : L →ₐ[K] L) = (g : L →ₐ[K] L)

[riccardobrasca]

Are these answers written by an LLM?

[yuanyi-350]

The initial commit was LLM-generated, but I made the subsequent changes myself based on your feedback. Currently, LLMs just don't understand defeq abuse.

[yuanyi-350]

The state analysis below is the experimental workflow I typed out manually. If I were to automate this part and provide this kind of information for every PR, do you think it would significantly reduce occurrences of defeq abuse?

[riccardobrasca]

There are already various discussion on Zulip about this, it's not completely clear how much of defeq abuse we want, so we currently decide case by case. Anyway this PR lgtm, thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Build