From 30bcd7cdab07b036dd1e44ea52ee23d7aeaeb814 Mon Sep 17 00:00:00 2001 From: Chris Birkbeck Date: Wed, 24 Jun 2026 20:51:12 +0100 Subject: [PATCH] =?UTF-8?q?cleanup(#4480):=20FltRegularBernoulli=20Furtwae?= =?UTF-8?q?ngler/ArtinHasse/DworkCoeffLeadingTermCongruence.lean=20?= =?UTF-8?q?=E2=80=94=20simpa=20best-API=20trim?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Full /cleanup (statement-preserving; no EXISTING statement token changed — only one proof-internal simpa line differs; every signature token-identical; no instance binders removed; no new helpers). sorryAx STEP-0 GATE PASSED: all 7 decls in BernoulliRegular.Furtwaengler [propext, Classical.choice, Quot.sound] — not OSKR-tainted (upstream ArtinHasse/Dwork infrastructure). (1) Best-mathlib-API / simp-set trim (×1): L145 in pow_sub_pow_mem_pow_succ_of_sub_mem_sq — simpa [pow_add, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hmul → simpa [Ideal.IsTwoSided.pow_add] using hmul (drops 3 redundant Nat.add_* normalization lemmas + switches to the ideal-specific Ideal.IsTwoSided.pow_add, matching the existing in-file convention 5 lines below at L150). PROBED+REVERTED (load-bearing, correctly kept): 3× simp → simp only (the convert…using 1; simp[…]; ring blocks in the three *_lt_ell_leading theorems — bare simp normalizes Nat.succ/Nat.factorial forms ring depends on; simp only left an unclosable goal); the change … ∈ I^((n+1)+1) on L149 (without it simpa [Ideal.IsTwoSided.pow_add] over-applies pow_add to both sides → I^n*I*I vs I^(n+1)*I^1 mismatch). NOT touched (correctly KEPT — used here): universe u v w (Type u/v/w used — contrast sibling #4479 where it was dead); open scoped NumberField (𝓞 used — contrast #4479); public imports (re-exported interface); the repeated 5-line instance-binder block (a variable-collapse would risk binder reorder/non-token-identical signatures + theorem #4 is a generic lemma not using them). +1/−1. decl-count unchanged (7); module green by name (3578 jobs); axioms on touched decl pow_sub_pow_mem_pow_succ_of_sub_mem_sq [propext, Classical.choice, Quot.sound]; zero new sorry; no statement token-changed; no residue (probe stripped, tail intact end Furtwaengler/end BernoulliRegular/end). Co-Authored-By: Claude Opus 4.8 (1M context) --- .../ArtinHasse/DworkCoeffLeadingTermCongruence.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/projects/FltRegularBernoulli/BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/ArtinHasse/DworkCoeffLeadingTermCongruence.lean b/projects/FltRegularBernoulli/BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/ArtinHasse/DworkCoeffLeadingTermCongruence.lean index c59c890c9..3cb3e2721 100644 --- a/projects/FltRegularBernoulli/BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/ArtinHasse/DworkCoeffLeadingTermCongruence.lean +++ b/projects/FltRegularBernoulli/BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/ArtinHasse/DworkCoeffLeadingTermCongruence.lean @@ -142,7 +142,7 @@ theorem pow_sub_pow_mem_pow_succ_of_sub_mem_sq have hleft : γ ^ n * (γ - π) ∈ I ^ (n + 2) := by have hmul : γ ^ n * (γ - π) ∈ I ^ n * I ^ 2 := Ideal.mul_mem_mul hγn hγπ - simpa [pow_add, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hmul + simpa [Ideal.IsTwoSided.pow_add] using hmul have hright : (γ ^ n - π ^ n) * π ∈ I ^ (n + 2) := by have hmul : (γ ^ n - π ^ n) * π ∈ I ^ (n + 1) * I ^ 1 := Ideal.mul_mem_mul ih (by simpa using hπ)