[#14519] 9077, with options, downstream - #10
Draft
downstream-lean4[bot] wants to merge 2 commits into
Draft
Conversation
downstream-lean4
Bot
added
the
adaptation
Contributor
Author
Build report for Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/14248Unchanged
|
snapshot
cleanup using inferInstanceAs
remove unnecessary options
fix WithLawson proof level, remove instanceTypes option
IsLawson.toT1Space accidentally elaborated one synonym level too high
(WithScott (WithLawson α)): the rw matched first-order with
?α := WithLawson α and the proof only closed because ambient α-level
instances were accepted into stacked-type slots. Pin the rewrite with
(α := α) and pass isClosed_Iic (a := WithScott.toScott a) so Iic
elaborates at WithScott α with its real instances.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
restrict simps to data fields on exteriorPower.relations, remove instanceTypes option
The @[simps]-generated relations_G/relations_R rewrite the *types*
(relations R ι M).G/.R to their definitional unfoldings; dsimp then
splits instance-carrying terms across the semireducible boundary,
which the instance-typed metavariable check (lean4#9077) rejects.
Generate only the relation projection lemma; the dropped lemmas have
no users in Mathlib.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
make Equiv.subtypeNeSumPUnit instances-transparent, remove instanceTypes option
Define it as a direct structure literal instead of a composition of
Equivs, and use Sum.casesOn instead of Sum.elim (both Equiv.trans and
Sum.elim are semireducible), so that subtypeNeSumPUnit i₀ (.inl i)
reduces to ↑i at .instances transparency. This lets the reindexed
AddCommMonoid family in PiTensorProduct.equivPiTensorComplSingletonTensor
match without the backward.isDefEq.instanceTypes escape hatch.
Generators.lean is the definition's only consumer.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
reinstate exteriorPower.relations simps lemmas, fix proofs locally instead
Dropping relations_G/relations_R was an API change; even unused in
Mathlib they are public API. Keep the full simps set and instead keep
the two forms aligned inside relationsSolutionEquiv: exclude the
type-rewriting lemmas from the dsimp calls, and re-type the invFun
goals' head at ι → M with a show (the goal mixes the .G-typed head
from the Solution field with the honest body exposed by iota).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
wrap RestrictScalars add-instances via inferInstanceAs, remove 3 instanceTypes options
The rejected assignment in the RepresentationTheory sites is the raw
AddCommMonoid/AddCommGroup reuse (:= I): synthesis of
Module k (RestrictScalars k k[G] M) unfolds the reducible
Module.restrictScalars abbrev, exposing Module.compHom's AddCommMonoid
metavariable, which unification fills across the semireducible synonym
boundary. Wrapping the two reuse instances with inferInstanceAs makes
them packed instances that collapse at .instances transparency (same
pattern as aff3b0cfb0 for Additive/Multiplicative); the compHom-built
Module instance is untouched. Unblocks Irreducible, Rep/Iso and
Semisimple; the asModule-side files keep their options (their failures
are statement-level structure-field reuse, not instance definitions).
Verified with a full Mathlib build.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
retype CompatibleSMul hypothesis at the Cotangent form, remove instanceTypes option
The have in KaehlerDifferential.D was typed at the synonym Ω[S⁄R]
while the map_smul_of_tower rewrites go through Ideal.toCotangent,
whose codomain is the honest (ideal R S).Cotangent; the two agree only
by unfolding the semireducible KaehlerDifferential def, which the
instance-typed metavariable check (lean4#9077) refuses.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
state inv_pair₂ at φ(p, k), remove instanceTypes option
The semilinear coercion synthesizes RingHomInvPair at the notation form
φ(p, k) (a semireducible def wrapping ↑(FractionRing.frobenius p k)),
but inv_pair₂ was stated at the raw coercion, so matching it
cross-assigned across the wrapper. Align with inv_pair₁, which already
uses φ(p, k).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
pin coercion implicit arguments, remove 2 instanceTypes options
Distinct mechanism from the usual rejected-assignment sites: nothing is
rejected, but the AlgHom→RingHom / FunLike coercions' implicit type
arguments are no longer inferred by unification (a side effect of the
lean4#9077 spine marking), leaving eval₂Hom's source ring and
tensorEquivSum's four type arguments unsolved ("Function expected").
Pin them explicitly, matching the fully-applied forms already used
elsewhere in the file.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
spell the units quotient subgroup in comap form, remove instanceTypes option
The rfl-lemma composed mk' at principalUnitGroup.subgroupOf unitGroup
against an equiv defined at principalUnitGroup.comap unitGroup.subtype;
subgroupOf is a semireducible wrapper of the latter, so identifying the
two quotients cross-assigned the quotient's MulOneClass instance. Use
the comap spelling the equiv (and its ker lemma) already use.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
pin ker_liftQ_eq_bot' submodule argument, remove instanceTypes option
The proof mixed the goal's torsionBy R M b with the proof term's
inferred ker (lsmul R M b) form of the same submodule (defeq only by
unfolding two semireducible defs), cross-assigning the quotient Module
instance. Passing the explicit argument in the goal's form keeps
everything at one spelling.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
keep instance-carrying forms aligned in Smooth/Unramified proofs, remove 4 instanceTypes options
Four sites, one family: a simp/convert!/coercion step re-synthesizes an
instance across a semireducible boundary (the local-instance algebra
towers on MvPolynomial/Polynomial, the Shrink.ringEquiv synonym inside
a quotient's Semiring index, the D.subalgebra R scalar tower). Fixes
are proof-local: pin scalarRTensorAlgEquiv's implicits, rewrite through
includeRight with map_pow instead of convert!/simp, feed the comap
ideal pre-unfolded and drop Shrink.ringEquiv from the simpa set, and
show-retype the kernel membership goal to reuse the already-elaborated
map.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
synthesize the reduct's structure instead of pinning M.struc, remove instanceTypes option
Passing M.struc explicitly pinned the IsExpansionOn goal's structure
index at the ↑M-typed instance, forcing every candidate to cross-assign
across the semireducible ModelType.reduct/subtheoryModel carriers. Add
the honest L[[α]].Structure on the reduct carrier as a letI and let
both instance arguments be synthesized against it.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
avoid unfolding the valuation inside the WithVal index, remove instanceTypes option
simp only [Rat.padicValuation, ...] delta-unfolded the valuation inside
the WithVal (Rat.padicValuation p) type index of the goal but not of h,
splitting embedding ↑γ into two atoms that agree only above .instances.
Rewrite only the applied position (rw [show ... from rfl]) and simp h
separately, keeping the index folded.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
narrow two instanceTypes options to respectTransparency
The basis/basis_inr failures at the Extension.Ring/MvPolynomial
projection boundary only need the older respectTransparency relaxation
(this file's baseline idiom on ~18 declarations): with it, the ring
tower resolves before any instance metavariable is created, so the
lean4#9077 instance-typed check stays fully active on these
declarations. The third site keeps instanceTypes false (its
restrictScalars simp step re-synthesizes Cotangent's module structure
across the boundary).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
fixes after rebasing
revert Claude's 'fixes'
fixes after rebasing
elaborate trace-based explanation of the 'MonoCoprod Schema' issue
remove obsolete implicit_reducible annotations?
fix stuff by reverting unnecessary stuff
more trace-postprocessing-based investigations
five more investigations
five more (AI-based) analysis preparations
fixes after switching to markOrSynth
re-analyzed all the cases with postprocessed traces that still required 'none'
AI-analyzed 5 more sites and hand-fixed LinearMap.Index after the analysis
review the other four
cleanups and corrections
analysis guide
cleanups
cleanup
clean up more explanations
fix
AI-based shortenings
fix long line
fix
shorten TopCatAdjunction
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is the adaptation PR for leanprover/lean4#14519.