diff --git a/lean-toolchain b/lean-toolchain index 728ce7a44..c9f1db5d3 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-07-22 +leanprover/lean4-pr-releases:pr-release-14519-3802ee9 diff --git a/mathlib4/ANALYSIS_GUIDE.md b/mathlib4/ANALYSIS_GUIDE.md new file mode 100644 index 000000000..0a6b9a1cf --- /dev/null +++ b/mathlib4/ANALYSIS_GUIDE.md @@ -0,0 +1,167 @@ +# Writing a good `instanceTypes` site analysis + +Guidance for agents documenting why a Mathlib site needs +`set_option backward.isDefEq.instanceTypes "none"` (the strict instance-typed-mvar check from +lean4 PR #9077). Distilled from the analyses in e.g. `Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean`, +`Mathlib/LinearAlgebra/AffineSpace/Ordered.lean`, `Mathlib/RingTheory/Kaehler/JacobiZariski.lean`. + +## The `markOrSynth` outcome, in words + +The project default is `"markOrSynth"` (set in the lakefile's `leanOptions`, NOT the register +default). An assignment to an instance-typed mvar succeeds if either +1. the **direct type check** accepts: the value's type matches the mvar's type at `.instances` + transparency (spine mvars admissible), or +2. the **fallback**: the instance is synthesized for the mvar's type, and the candidate value is + defeq to the **synthesized instance**. +A site needs `"none"` only when both fail. The write-up must say, in these words, where the +failure lands: the direct type check rejects, and then either *the fallback synthesis fails*, or +*synthesis succeeds but the candidate is not defeq to the synthesized instance*. Spell the path +out in self-contained prose — never letter/number codes for the paths. + +A site that also carries `respectTransparency false` deserves suspicion: that option suppresses +all `.implicit` bumps, so first-pass easy-case unifications and the fallback's +candidate-vs-synthesized comparison run at the ambient `.instances` transparency — often the +very strictness being worked around. An `implicit_reducible` annotation on the blocking synonym +frequently removes the need for BOTH options at once: with `respectTransparency` restored to +`true`, the bumped `.implicit` comparisons unfold the annotation. + +Classify every site as one of the **two underlying issues**: +- **Missing `implicit_reducible` annotation in Mathlib**: candidate and synthesized instance are + the same instance up to a synonym/projection spelling that merely fails to unfold at the + operative transparency. The real fix is an annotation (or a proof-local respelling). +- **Actual mismatch between unified and synthesized instances**: genuinely different instances + (e.g. TopCatAdjunction's coinduced topology vs `compactOpen`, not defeq at any transparency). + Re-synthesis would silently change the statement's meaning; the fix must respell the + statement/proof. + +## What the write-up is for + +A maintainer reading the file should be able to judge, without re-running anything, (a) what +exactly fails and why, (b) whether the failure is harmless-but-strict or a genuine defeq abuse, +and (c) what a real fix would look like. The write-up is **show-don't-tell**: one compact +guarded trace demonstrates the mechanism; prose is reduced to a few pointer lines. There are no +long comment blocks. + +## In-file format (show-don't-tell) + +Exemplars: `Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean`, +`Mathlib/CategoryTheory/Abelian/Subobject.lean`, `Mathlib/Condensed/TopCatAdjunction.lean`. + +- Module-docstring headers structure the site: `/-! # Issue -/` (or `# First issue: \`decl\``), + then the **real declaration first** (its options unchanged), then `/-! ## Explanation -/`. +- The Explanation is at most a few comment lines (which synonym boundary, cross-reference, + which of the two underlying issues) plus **one** `#guard_msgs`-guarded `postprocess_traces` + demo: a copy of the declaration as an `example`, pinned + `set_option backward.isDefEq.instanceTypes "markOrSynth"`, with + `trace.Meta.synthInstance`, `trace.Meta.isDefEq`, `trace.Meta.isDefEq.printTransparency`, + `trace.Meta.isDefEq.assign.checkTypes` scoped inside the proof at the decisive step. +- The trace must show the decisive `isDefEq.assign.checkTypes` node **with its internals**: the + direct `.instances` type check, whether the fallback re-synthesis succeeds (elide its subtree: + `[Meta.synthInstance] ✅ … (truncated)`), and whether the following unification of the + unified vs synthesized instance succeeds. That trace answers the mark/markOrSynth questions + by itself. +- Canonical postprocessor chain (copy the `private meta partial def elideBelow` helper, and + `dropSubtrees` where needed, from an exemplar): + `filterSubtrees (fun x => (ofClass `Meta.isDefEq.assign.checkTypes x) <&&> failed x) + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> succeeded x)` + plus site-specific pruning disjuncts. Guards of ~60–110 lines are acceptable. +- Sites whose real declaration compiles at `"markOrSynth"` (fallback-rescued or lever-fixed): + the demo reproduces the *problem form* (without the lever/proof-local fix); if the decisive + checkTypes node succeeds overall, filter on `ofClass checkTypes` plus a `containsString` + instead of `failed`. +- Several sites sharing one cause: full trace at the primary site, few-line pointer comments at + the siblings. +- An optional `/-! # Fix -/` section holds a passing variant (lever example or respelled form) + only when the main trace cannot show it. +- Delete every other trace excerpt, counterfactual, and prose paragraph whose message the main + trace subsumes. Do not discuss the Prop-exemption. + +## Debugging workflow (Paul's recipe) + +Enable `trace.Meta.isDefEq` (+ `trace.Meta.isDefEq.printTransparency`), `trace.Meta.synthInstance`, +and `trace.Meta.isDefEq.assign.checkTypes` on the failing tactic. Then postprocess, usually as a +chain: start with a filter that keeps only the `synthInstance` trace tree for the instance of +interest, then `filterSubtrees` to expose the node of interest (e.g. a failing `checkTypes`) +*with its context*, and `elideBelow` (copy the helper from existing demo sections, e.g. +`Mathlib/FieldTheory/Galois/Profinite.lean`) to cut the tree below the — usually succeeding — +fallback instance synthesis inside `checkTypes`, keeping the trace manageable. + +Read the result against this decision tree: +- **A `checkTypes` node is marked failed** (the expected manifestation). Distinguish: + - the fallback synthesis for the mvar's expected type *fails*, or + - synthesis succeeds and the unification of synthesized vs unified instance fails — note the + transparency level at which it fails (this is what `printTransparency` is for). +- **Every mvar assignment succeeds**: unexpected — the toolchain change should manifest via a + failing `checkTypes`. Re-examine where the failure actually comes from before blaming the + option. + +## Evidence standards + +- **Every causal claim is trace-backed.** No "presumably" in the final prose. +- **Separate load-bearing from noise.** A ❌ that also occurs with the option *disabled* is + noise. Always produce one strict-mode and one option-on log and diff them; only failures + unique to strict mode can be load-bearing. +- **Find the diverging simp lemma by diffing** `trace.Meta.Tactic.simp.rewrite` counts between + the two modes — this localizes the failure to a lemma before you read any synthesis trace. +- **Substantiate defeq claims at the right transparency, on the exact terms from the rejected + assignment, not simplified stand-ins.** For the two *types*, use + `with_reducible_and_instances apply_rfl` (mirrors the check itself). For comparing the + *instance values* (candidate vs synthesized), use `with_implicit apply_rfl`. `with_reducible` + is the wrong level for both — do not use it as a proxy. Plain `apply_rfl` at default is the + counterfactual showing the assignment was harmless. +- **Two orthogonal facts, never conflated:** the check compares the instance mvar's *types* at + `.instances`; whether the instance *values* are defeq (and at what level) is a separate + question about whether the rejection is harmful. State both, separately. +- Pretty-printed-identical types can still desync in an implicit argument — check with + `pp.explicit` before concluding "the types look equal". + +## Demos + +- The single trace demo runs on an **actual copy of the failing declaration** (options flipped + so the behavior shows), never on a simplified stand-in. Do not hoist the failing synthesis + goal into a standalone `#synth`/`example` — the context of how elaboration arrived at that + synthInstance is part of the evidence. +- Scope traces to the single relevant tactic with `set_option trace.… true in` *inside* the + proof — this shrinks postprocessor filters to 1–2 disjuncts. +- Prune with `postprocess_traces` (`filterSubtrees`, `ofClass`, `containsString`, `failed`, + `>=>`), keeping the ancestry `synthInstance → apply → tryResolve → checkTypes` so the reader + sees *whose* mvar rejects. `containsString` sees full-name formatting: use several short + fragments joined with `<&&>` rather than one string crossing constant-name boundaries. +- Pin `#guard_msgs` via the PLACEHOLDER flow: write `error: PLACEHOLDER`, compile, splice the + `+`-lines from the mismatch diff back in, recompile to exit 0. Re-verify with + `-Dpp.unicode.fun=true` (editor and CLI print lambdas differently). +- **Keep guards small.** Drop `trace.Meta.isDefEq` when the checkTypes ❌ lines alone carry both + types; silence unrelated linters (`linter.unusedSimpArgs`, `linter.style.longLine`) with a + note in the prose if the linter output was itself evidence; `sorry`-scaffold induction + branches you are not demonstrating. Target ≲ 40 guard lines. + +## Pitfalls (all cost real time once) + +- `convert`/`congr` roll back failed branches (`commitWhen`) and **discard their traces** — + the substantive ❌ appears only when you trace the *follow-up* tactic (usually the closing + `simp`). +- `trace_state` always triggers the `unusedTactic` "does nothing" warning; it does not mean + the goal list is empty. +- Compile single files from the repo root: + `lake env lean -DmaxSynthPendingDepth=3 -Dpp.unicode.fun=true -Dbackward.isDefEq.instanceTypes=markOrSynth ` + — never `lake build`, and never from another working directory. The mode flag is NOT optional: + bare `lake env lean` runs the register default `"mark"`, not the lakefile's `"markOrSynth"`, + and the same site can fail under both modes *for different reasons*. Demos written into files + pin `set_option backward.isDefEq.instanceTypes "markOrSynth"` for the same reason. +- The `diagnostics`-mode "Workaround: …" messages for the fallback paths are emitted inside + `checkpointDefEq` (and often inside simp's speculative `tryResolve`) and get rolled back — + they usually never surface. Identify the failing path from the trace-tree shape instead: a + successful `[Meta.synthInstance] … result ` child nested under a ❌ + `Meta.isDefEq.assign.checkTypes` node means synthesis succeeded and the candidate-vs- + synthesized comparison failed. +- Error positions in long `have`/`suffices` chains are easy to misattribute — read the probe + file at the reported line instead of guessing which tactic failed. +- When replicating a `private` declaration in a probe, carry over *all* of the original site's + `set_option`s — elaboration can diverge wildly with a partial option set. + +## Style + +- Complete sentences, no arrow-chain shorthand in prose (arrows are fine inside quoted traces). +- Cross-references cite files, not survey-internal category letters. +- The demo section is named (`section InstanceTypesDemos`) and self-contained, so it can be + deleted wholesale once the underlying issue is fixed upstream. diff --git a/mathlib4/Mathlib/Algebra/Category/Grp/Colimits.lean b/mathlib4/Mathlib/Algebra/Category/Grp/Colimits.lean index bcef27d14..62c124715 100644 --- a/mathlib4/Mathlib/Algebra/Category/Grp/Colimits.lean +++ b/mathlib4/Mathlib/Algebra/Category/Grp/Colimits.lean @@ -11,6 +11,7 @@ public import Mathlib.CategoryTheory.ConcreteCategory.Elementwise public import Mathlib.Data.DFinsupp.BigOperators public import Mathlib.Data.DFinsupp.Small public import Mathlib.GroupTheory.QuotientGroup.Defs +meta import Lean.PostprocessTraces /-! # The category of additive commutative groups has all colimits. @@ -18,6 +19,7 @@ This file constructs colimits in the category of additive commutative groups, as quotients of finitely supported functions. -/ +open Lean.PostprocessTraces @[expose] public section @@ -301,6 +303,13 @@ namespace AddCommGrpCat open QuotientAddGroup +/-! +# Issue (Trivial Severity) + +Actually, the `respectTransparency false` "fixes it" already by *preventing* a bump. +However, the sustainable fix would be to fix the `lift_mk` rfl lemma. +-/ + set_option backward.isDefEq.respectTransparency false in set_option backward.defeqAttrib.useBackward true in /-- The categorical cokernel of a morphism in `AddCommGrpCat` @@ -321,8 +330,8 @@ noncomputable def cokernelIsoQuotient {G H : AddCommGrpCat.{u}} (f : G ⟶ H) : rfl inv_hom_id := by ext x - dsimp only [hom_comp, hom_ofHom, hom_zero, AddMonoidHom.coe_comp, coe_mk', - Function.comp_apply, AddMonoidHom.zero_apply, id_eq, lift_mk, hom_id, AddMonoidHom.coe_id] + dsimp only [hom_comp, hom_ofHom, hom_zero, AddMonoidHom.coe_comp, coe_mk', lift_mk, + Function.comp_apply, AddMonoidHom.zero_apply, id_eq, hom_id, AddMonoidHom.coe_id] exact QuotientAddGroup.induction_on (α := H) x <| cokernel.π_desc_apply f _ _ end AddCommGrpCat diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean index 63b60eb1d..24d1bebac 100644 --- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean +++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean @@ -39,6 +39,7 @@ to show that the two vanishing conditions `d_app` are equivalent). @[expose] public section + universe v u v₁ v₂ u₁ u₂ open CategoryTheory @@ -78,6 +79,13 @@ variable (d : M.Derivation φ) @[simp] lemma d_one (X : Dᵒᵖ) : d.d (X := X) 1 = 0 := by simpa using d.d_mul (X := X) 1 1 +/-! +# Issue (Low Severity) + +Has uncontroversial fix. +-/ + +set_option backward.isDefEq.instanceTypes "none" in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The postcomposition of a derivation by a morphism of presheaves of modules. -/ @@ -90,6 +98,27 @@ def postcomp (f : M ⟶ N) : N.Derivation φ where erw [d_app] rw [map_zero] +/-! +# Fix + +Two harmless implicit_reducible annotations. +Can even get rid of `erw`. +-/ +set_option allowUnsafeReducibility true +attribute [local implicit_reducible] + ModuleCat.restrictScalars + ModuleCat.RestrictScalars.obj' +in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option backward.defeqAttrib.useBackward true in +example (f : M ⟶ N) : N.Derivation φ where + d := (f.app _).hom.toAddMonoidHom.comp d.d + d_map {X Y} g x := by simpa using naturality_apply f g (d.d x) + d_app {X} a := by + dsimp + rw [d_app] + rw [map_zero] + /-- The universal property that a derivation `d : M.Derivation φ` must satisfy so that the presheaf of modules `M` can be considered as the presheaf of (relative) differentials of a presheaf of commutative rings `φ : S ⟶ F.op ⋙ R`. -/ diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean index 119610224..0cf4af20b 100644 --- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean +++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean @@ -9,10 +9,13 @@ public import Mathlib.CategoryTheory.Monoidal.Closed.Basic public import Mathlib.CategoryTheory.Linear.Yoneda public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric +meta import Lean.PostprocessTraces /-! # The monoidal closed structure on `Module R`. -/ +open Lean.PostprocessTraces + @[expose] public section universe v w x u @@ -76,6 +79,13 @@ theorem ihom_ev_app (M N : ModuleCat.{u} R) : apply TensorProduct.ext' apply monoidalClosed_uncurry +/-! +# Issue (Low Severity) + +Uncontroversial fix available. +-/ + +set_option backward.isDefEq.instanceTypes "none" in set_option backward.isDefEq.respectTransparency false in /-- Describes the unit of the adjunction `M ⊗ - ⊣ Hom(M, -)`. Given an `R`-module `N` this should define a map `N ⟶ Hom(M, M ⊗ N)`, which is given by flipping the arguments in the natural @@ -84,6 +94,31 @@ theorem ihom_coev_app (M N : ModuleCat.{u} R) : (ihom.coev M).app N = ModuleCat.ofHom₂ (TensorProduct.mk _ _ _).flip := rfl +/-! +# Fix + +Make `TensorProduct` implicit-reducible and remove `respectTransparency false`. +-/ + +set_option linter.style.longLine false +postprocess_traces + filterSubtrees (fun x => ofClass `Meta.synthInstance x <&&> containsString "Module R (TensorProduct" x) + >=> filterSubtrees (fun x => ofClass `Meta.isDefEq.assign.checkTypes x <&&> failed x) +in +attribute [local implicit_reducible] TensorProduct in +set_option linter.style.setOption false in +set_option trace.Meta.isDefEq.assign.checkTypes true in +set_option trace.Meta.synthInstance true in +set_option trace.Meta.isDefEq true in +set_option trace.Meta.isDefEq.printTransparency true in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +/-- Describes the unit of the adjunction `M ⊗ - ⊣ Hom(M, -)`. Given an `R`-module `N` this should +define a map `N ⟶ Hom(M, M ⊗ N)`, which is given by flipping the arguments in the natural +`R`-bilinear map `M ⟶ N ⟶ M ⊗ N`. -/ +example (M N : ModuleCat.{u} R) : + (ihom.coev M).app N = ModuleCat.ofHom₂ (TensorProduct.mk _ _ _).flip := + rfl + theorem monoidalClosed_pre_app {M N : ModuleCat.{u} R} (P : ModuleCat.{u} R) (f : N ⟶ M) : (MonoidalClosed.pre f).app P = ofHom (homLinearEquiv.symm.toLinearMap ∘ₗ LinearMap.lcomp _ _ f.hom ∘ₗ homLinearEquiv.toLinearMap) := diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean index e7f98beb3..5093daf19 100644 --- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean +++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean @@ -7,6 +7,8 @@ module public import Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed +-- imported only for the `InstanceTypesDemos` section at the end of this file +meta import Lean.PostprocessTraces /-! # The monoidal category structure on presheaves of modules @@ -26,6 +28,7 @@ This contribution was created as part of the AIM workshop @[expose] public section open CategoryTheory MonoidalCategory BraidedCategory Category Limits +open Lean.PostprocessTraces universe v u v₁ u₁ @@ -40,6 +43,23 @@ namespace Monoidal variable (M₁ M₂ M₃ M₄ : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) +/- +"markOrSynth" analysis: + +Affected declarations: `tensorObjMap`, `tensorObj_map_tmul`. + +* instance types with `R.obj X` vs. `(R ⋙ forget₂ CommRingCat RingCat).obj X` (`CommRingCat`) +* `respectTransparency false` -> comparison of synthesized/unified at instance transparency + +fix: + +mark `ModuleCat.RestrictScalars.obj'` and `ModuleCat.restrictScalars` implicit-reducible, +remove `respectTransparency false`. +-/ + +/-! # First issue: `tensorObjMap` -/ + +set_option backward.isDefEq.instanceTypes "none" in set_option backward.isDefEq.respectTransparency false in /-- Auxiliary definition for `tensorObj`. -/ noncomputable def tensorObjMap {X Y : Cᵒᵖ} (f : X ⟶ Y) : M₁.obj X ⊗ M₂.obj X ⟶ @@ -56,6 +76,156 @@ noncomputable def tensorObjMap {X Y : Cᵒᵖ} (f : X ⟶ Y) : M₁.obj X ⊗ M rw [map_add, TensorProduct.tmul_add]) (by intro a m₁ m₂; dsimp; erw [M₂.map_smul, TensorProduct.tmul_smul (r := R.map f a)]; rfl) +/-! ## Explanation -/ + +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +/-- +error: failed to synthesize instance of type class + TensorProduct.CompatibleSMul ↑(R.obj Y) ↑(R.obj Y) ↑(M₁.obj Y) ↑(M₂.obj Y) +--- +error: unsolved goals +C : Type u_1 +inst✝ : Category.{v_1, u_1} C +R : Cᵒᵖ ⥤ CommRingCat +M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat) +X Y : Cᵒᵖ +f : X ⟶ Y +a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X) +m₁ : ↑(M₁.obj X) +m₂ : ↑(M₂.obj X) +⊢ TensorProduct.CompatibleSMul ↑(R.obj Y) ↑(R.obj Y) ↑(M₁.obj Y) ↑(M₂.obj Y) +--- +trace: [Meta.synthInstance] ❌️ TensorProduct.CompatibleSMul ↑(R.obj Y) ↑(R.obj Y) ↑(M₁.obj Y) ↑(M₂.obj Y) + [Meta.synthInstance.apply] ❌️ apply @TensorProduct.CompatibleSMul.isScalarTower to TensorProduct.CompatibleSMul + ↑(R.obj Y) ↑(R.obj Y) ↑(M₁.obj Y) ↑(M₂.obj Y) + [Meta.synthInstance.tryResolve] ❌️ TensorProduct.CompatibleSMul ↑(R.obj Y) ↑(R.obj Y) ↑(M₁.obj Y) + ↑(M₂.obj Y) ≟ TensorProduct.CompatibleSMul ?m.272 ?m.273 ?m.276 ?m.277 + [Meta.isDefEq] ❌️ [instances] TensorProduct.CompatibleSMul ↑(R.obj Y) ↑(R.obj Y) ↑(M₁.obj Y) + ↑(M₂.obj Y) =?= TensorProduct.CompatibleSMul ?m.272 ?m.273 ?m.276 ?m.277 + [Meta.isDefEq] ❌️ [instances] ModuleCat.instModuleCarrierObjRestrictScalars.toDistribMulAction =?= ?m.285 + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.285 : DistribMulAction ↑(R.obj Y) + ↑(M₂.obj + Y)) := (ModuleCat.instModuleCarrierObjRestrictScalars.toDistribMulAction : DistribMulAction + ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y) + ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj + (M₂.obj Y))) + [Meta.isDefEq] ❌️ [instances] DistribMulAction ↑(R.obj Y) + ↑(M₂.obj + Y) =?= DistribMulAction ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y) + ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj + (M₂.obj Y)) + [Meta.isDefEq] ❌️ [instances] ↑(R.obj Y) =?= ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y) + [Meta.isDefEq] ❌️ [instances] (R.obj Y).1 =?= ((R ⋙ forget₂ CommRingCat RingCat).obj Y).1 + [Meta.isDefEq.onFailure] ❌️ (R.obj Y).1 =?= ((R ⋙ forget₂ CommRingCat RingCat).obj Y).1 + [Meta.isDefEq.onFailure] ❌️ DistribMulAction ↑(R.obj Y) + ↑(M₂.obj + Y) =?= DistribMulAction ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y) + ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj + (M₂.obj Y)) + [Meta.synthInstance] ✅️ DistribMulAction ↑(R.obj Y) ↑(M₂.obj Y) (truncated) + [Meta.isDefEq] ❌️ [instances] ModuleCat.instModuleCarrierObjRestrictScalars.toDistribMulAction =?= (M₂.obj + Y).isModule.toDistribMulAction + [Meta.isDefEq] ❌️ [instances] ModuleCat.instModuleCarrierObjRestrictScalars.1 =?= (M₂.obj Y).isModule.1 + [Meta.isDefEq] ❌️ [instances] { toSMul := ModuleCat.instModuleCarrierObjRestrictScalars._aux_1, + mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ } =?= (M₂.obj Y).isModule.1 + [Meta.isDefEq] ❌️ [instances] DistribMulAction ↑(R.obj Y) + ↑(M₂.obj + Y) =?= DistribMulAction ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y) + ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj + (M₂.obj Y)) + [Meta.isDefEq] ❌️ [instances] ↑(R.obj Y) =?= ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y) + [Meta.isDefEq] ❌️ [instances] (R.obj Y).1 =?= ((R ⋙ forget₂ CommRingCat RingCat).obj Y).1 + [Meta.isDefEq.onFailure] ❌️ (R.obj Y).1 =?= ((R ⋙ forget₂ CommRingCat RingCat).obj Y).1 + [Meta.isDefEq.onFailure] ❌️ DistribMulAction ↑(R.obj Y) + ↑(M₂.obj + Y) =?= DistribMulAction ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y) + ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj + (M₂.obj Y)) + [Meta.isDefEq.onFailure] ❌️ { toSMul := ModuleCat.instModuleCarrierObjRestrictScalars._aux_1, + mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ } =?= (M₂.obj Y).isModule.1 + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.285 : DistribMulAction ↑(R.obj Y) + ↑(M₂.obj + Y)) := ({ toSMul := ModuleCat.instModuleCarrierObjRestrictScalars._aux_1, mul_smul := ⋯, + one_smul := ⋯, smul_zero := ⋯, + smul_add := + ⋯ } : DistribMulAction ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y) + ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj + (M₂.obj Y))) + [Meta.isDefEq] ❌️ [instances] DistribMulAction ↑(R.obj Y) + ↑(M₂.obj + Y) =?= DistribMulAction ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y) + ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj + (M₂.obj Y)) + [Meta.isDefEq] ❌️ [instances] ↑(R.obj Y) =?= ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y) + [Meta.isDefEq.onFailure] ❌️ DistribMulAction ↑(R.obj Y) + ↑(M₂.obj + Y) =?= DistribMulAction ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y) + ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj + (M₂.obj Y)) + [Meta.synthInstance] ✅️ DistribMulAction ↑(R.obj Y) ↑(M₂.obj Y) (truncated) + [Meta.isDefEq] ❌️ [instances] { toSMul := ModuleCat.instModuleCarrierObjRestrictScalars._aux_1, + mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, + smul_add := ⋯ } =?= (M₂.obj Y).isModule.toDistribMulAction + [Meta.isDefEq] ❌️ [instances] { toSMul := ModuleCat.instModuleCarrierObjRestrictScalars._aux_1, + mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ } =?= (M₂.obj Y).isModule.1 + [Meta.isDefEq] ❌️ [instances] DistribMulAction ↑(R.obj Y) + ↑(M₂.obj + Y) =?= DistribMulAction ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y) + ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj + (M₂.obj Y)) + [Meta.isDefEq] ❌️ [instances] ↑(R.obj Y) =?= ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y) + [Meta.isDefEq] ❌️ [instances] (R.obj Y).1 =?= ((R ⋙ forget₂ CommRingCat RingCat).obj Y).1 + [Meta.isDefEq.onFailure] ❌️ (R.obj Y).1 =?= ((R ⋙ forget₂ CommRingCat RingCat).obj Y).1 + [Meta.isDefEq.onFailure] ❌️ DistribMulAction ↑(R.obj Y) + ↑(M₂.obj + Y) =?= DistribMulAction ↑((R ⋙ forget₂ CommRingCat RingCat).obj Y) + ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj + (M₂.obj Y)) + [Meta.isDefEq.onFailure] ❌️ { toSMul := ModuleCat.instModuleCarrierObjRestrictScalars._aux_1, + mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ } =?= (M₂.obj Y).isModule.1 +-/ +#guard_msgs in +postprocess_traces + filterSubtrees (fun x => (ofClass `Meta.isDefEq.assign.checkTypes x) <&&> failed x) + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> succeeded x) +in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option backward.isDefEq.respectTransparency false in +/-- `tensorObjMap` -/ +noncomputable example {X Y : Cᵒᵖ} (f : X ⟶ Y) : M₁.obj X ⊗ M₂.obj X ⟶ + (ModuleCat.restrictScalars (R.map f).hom).obj (M₁.obj Y ⊗ M₂.obj Y) := + ModuleCat.MonoidalCategory.tensorLift (fun m₁ m₂ ↦ M₁.map f m₁ ⊗ₜ M₂.map f m₂) + (by + intro m₁ m₁' m₂ + dsimp +instances + rw [map_add, TensorProduct.add_tmul]) + (by intro a m₁ m₂; dsimp; erw [M₁.map_smul]; rfl) + (by + intro m₁ m₂ m₂' + dsimp +instances + rw [map_add, TensorProduct.tmul_add]) + (by + intro a m₁ m₂ + dsimp + erw [M₂.map_smul] + (set_option trace.Meta.synthInstance true in + set_option trace.Meta.isDefEq true in + set_option trace.Meta.isDefEq.printTransparency true in + set_option trace.Meta.isDefEq.assign.checkTypes true in + erw [TensorProduct.tmul_smul (r := R.map f a)]) -- fails on the `erw` + rfl) + set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The tensor product of two presheaves of modules. -/ @@ -75,6 +245,14 @@ noncomputable def tensorObj : PresheafOfModules (R ⋙ forget₂ _ _) where variable {M₁ M₂ M₃ M₄} +/-! # Second issue: `tensorObj_map_tmul` -/ + +-- Needs `instanceTypes "none"` for the same `R.obj Y` (`CommRingCat`) vs +-- `(R ⋙ forget₂ CommRingCat RingCat).obj Y` (`RingCat`) ring-carrier synonym as `tensorObjMap` +-- above: here the `Module ↑(R.obj Y) ↑((restrictScalars …).obj (M₁.obj Y))` needed to type the +-- coercion is unsynthesizable because its `Ring ↑(R.obj Y)` slot rejects (leg (c)) the +-- `RingCat`-bundled instance the goal carries. See the analysis before `tensorObjMap`. +set_option backward.isDefEq.instanceTypes "none" in set_option backward.isDefEq.respectTransparency false in @[simp] lemma tensorObj_map_tmul {X Y : Cᵒᵖ} (f : X ⟶ Y) (m₁ : M₁.obj X) (m₂ : M₂.obj X) : @@ -83,6 +261,95 @@ lemma tensorObj_map_tmul {X Y : Cᵒᵖ} (f : X ⟶ Y) (m₁ : M₁.obj X) (m₂ (ModuleCat.Hom.hom (R := ↑(R.obj X)) ((tensorObj M₁ M₂).map f)) (m₁ ⊗ₜ[R.obj X] m₂) = M₁.map f m₁ ⊗ₜ[R.obj Y] M₂.map f m₂ := rfl +/-! ## Explanation: -/ + +/-- Keeps the `checkTypes` rejection head lines (both types) but drops their verbose +fallback-synthesis subtrees, so the trace demo stays small. -/ +private meta partial def dropCheckTypesChildren (t : TraceTree) : TraceTree := + if t.cls? == some `Meta.isDefEq.assign.checkTypes then t.withChildren #[] + else t.withChildren (t.children.map dropCheckTypesChildren) + +set_option linter.style.longLine false in +/-- +error: failed to synthesize instance of type class + Module ↑(R.obj Y) + ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj (M₁.obj Y)) +--- +trace: [Meta.synthInstance] ❌️ Module ↑(R.obj Y) + ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj (M₁.obj Y)) + [Meta.synthInstance.apply] ❌️ apply @ModuleCat.isModule to Module ↑(R.obj Y) + ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj (M₁.obj Y)) + [Meta.synthInstance.tryResolve] ❌️ Module ↑(R.obj Y) + ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj + (M₁.obj Y)) ≟ Module ?m.226 ↑?m.228 + [Meta.isDefEq] ❌️ Module ↑(R.obj Y) + ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj + (M₁.obj Y)) =?= Module ?m.226 ↑?m.228 + [Meta.isDefEq] ❌️ ↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).obj + (M₁.obj Y)) =?= ↑?m.228 + [Meta.isDefEq] ❌️ RingCat.instRingObjForgetRingHomCarrier =?= ?m.227 + [Meta.isDefEq] RingCat.instRingObjForgetRingHomCarrier [nonassignable] =?= ?m.227 [assignable] + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.227 : Ring + ↑(R.obj + Y)) := (RingCat.instRingObjForgetRingHomCarrier : Ring + ((forget RingCat).obj ((R ⋙ forget₂ CommRingCat RingCat).obj X))) + [Meta.isDefEq] ❌️ Ring + ↑(R.obj Y) =?= Ring ((forget RingCat).obj ((R ⋙ forget₂ CommRingCat RingCat).obj X)) + [Meta.isDefEq] ❌️ ↑(R.obj Y) =?= (forget RingCat).obj ((R ⋙ forget₂ CommRingCat RingCat).obj X) + [Meta.isDefEq] ❌️ (R.obj Y).1 =?= (forget RingCat).1 ((R ⋙ forget₂ CommRingCat RingCat).obj X) + [Meta.isDefEq] ❌️ (R.obj Y).1 =?= ToType ((R ⋙ forget₂ CommRingCat RingCat).obj X) + [Meta.isDefEq] ❌️ (R.obj Y).1 =?= ↑((R ⋙ forget₂ CommRingCat RingCat).obj X) + [Meta.isDefEq] ❌️ (R.obj Y).1 =?= ((R ⋙ forget₂ CommRingCat RingCat).obj X).1 + [Meta.isDefEq.onFailure] ❌️ (R.obj Y).1 =?= ((R ⋙ forget₂ CommRingCat RingCat).obj X).1 + [Meta.isDefEq.onFailure] ❌️ Ring + ↑(R.obj Y) =?= Ring ((forget RingCat).obj ((R ⋙ forget₂ CommRingCat RingCat).obj X)) + [Meta.synthInstance] ✅️ Ring ↑(R.obj Y) (truncated) + [Meta.isDefEq] ❌️ RingCat.instRingObjForgetRingHomCarrier =?= CommRingCat.instCommRingObjForgetRingHomCarrier.toRing + [Meta.isDefEq] ❌️ ((R ⋙ forget₂ CommRingCat RingCat).obj + X).ring =?= CommRingCat.instCommRingObjForgetRingHomCarrier.toRing + [Meta.isDefEq] ❌️ ((R ⋙ forget₂ CommRingCat RingCat).obj + X).2 =?= CommRingCat.instCommRingObjForgetRingHomCarrier.toRing + [Meta.isDefEq] ❌️ ((R ⋙ forget₂ CommRingCat RingCat).obj + X).2 =?= CommRingCat.instCommRingObjForgetRingHomCarrier.1 + [Meta.isDefEq.onFailure] ❌️ ((R ⋙ forget₂ CommRingCat RingCat).obj + X).2 =?= CommRingCat.instCommRingObjForgetRingHomCarrier.1 + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.227 : Ring + ↑(R.obj + Y)) := (((R ⋙ forget₂ CommRingCat RingCat).obj + X).2 : Ring ((R ⋙ forget₂ CommRingCat RingCat).obj X).1) + [Meta.isDefEq] ❌️ Ring ↑(R.obj Y) =?= Ring ((R ⋙ forget₂ CommRingCat RingCat).obj X).1 + [Meta.isDefEq] ❌️ ↑(R.obj Y) =?= ((R ⋙ forget₂ CommRingCat RingCat).obj X).1 + [Meta.isDefEq] ❌️ (R.obj Y).1 =?= ((R ⋙ forget₂ CommRingCat RingCat).obj X).1 + [Meta.isDefEq.onFailure] ❌️ (R.obj Y).1 =?= ((R ⋙ forget₂ CommRingCat RingCat).obj X).1 + [Meta.isDefEq.onFailure] ❌️ Ring ↑(R.obj Y) =?= Ring ((R ⋙ forget₂ CommRingCat RingCat).obj X).1 + [Meta.synthInstance] ✅️ Ring ↑(R.obj Y) (truncated) + [Meta.isDefEq] ❌️ ((R ⋙ forget₂ CommRingCat RingCat).obj + X).2 =?= CommRingCat.instCommRingObjForgetRingHomCarrier.toRing + [Meta.isDefEq] ❌️ ((R ⋙ forget₂ CommRingCat RingCat).obj + X).2 =?= CommRingCat.instCommRingObjForgetRingHomCarrier.1 + [Meta.isDefEq.onFailure] ❌️ ((R ⋙ forget₂ CommRingCat RingCat).obj + X).2 =?= CommRingCat.instCommRingObjForgetRingHomCarrier.1 +-/ +#guard_msgs in +postprocess_traces + filterSubtrees (fun x => (ofClass `Meta.synthInstance.apply x) + <&&> (containsString "ModuleCat.isModule" x) <&&> (containsString "M₁.obj Y" x)) + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> (containsString "Ring " x)) + >=> filterSubtrees (fun x => (failed x) <&&> (containsString "instRingObjForget" x)) +in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option backward.isDefEq.respectTransparency false in +set_option trace.Meta.synthInstance true in +set_option trace.Meta.isDefEq true in +set_option trace.Meta.isDefEq.assign.checkTypes true in +example {M₁ M₂ : PresheafOfModules.{u} (R ⋙ forget₂ _ _)} {X Y : Cᵒᵖ} (f : X ⟶ Y) + (m₁ : M₁.obj X) (m₂ : M₂.obj X) : + DFunLike.coe (α := (M₁.obj X ⊗ M₂.obj X :)) + (β := fun _ ↦ (ModuleCat.restrictScalars (R.map f).hom).obj (M₁.obj Y ⊗ M₂.obj Y)) + (ModuleCat.Hom.hom (R := ↑(R.obj X)) + ((_root_.PresheafOfModules.Monoidal.tensorObj M₁ M₂).map f)) (m₁ ⊗ₜ[R.obj X] m₂) = + M₁.map f m₁ ⊗ₜ[R.obj Y] M₂.map f m₂ := rfl + set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The tensor product of two morphisms of presheaves of modules. -/ @@ -244,4 +511,84 @@ instance (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) : PreservesColimitsOfSize.{u, u} (tensorRight F) := preservesColimits_of_natIso (tensorLeftIsoTensorRight F) +section InstanceTypesDemos +/-! +Guarded demonstrations for the two `backward.isDefEq.instanceTypes "none"` sites above. +The trace demo pins `"markOrSynth"` (the `lakefile.lean` project default; a bare +`lake env lean` would otherwise fall back to the toolchain register default `"mark"`). +`with_reducible rfl` is used as a proxy for the `.instances` transparency the instance-type +check runs at: it accepts nothing below `.default`, which is exactly where the two ring +spellings and the instances built on them diverge. Delete this whole section once the +`R.obj`/`forget₂` carrier synonym is resolved upstream. +-/ +open Lean.PostprocessTraces + +namespace PresheafOfModules.Monoidal + +-- Demo 1 (shared root cause). The ring carriers, and the `Ring` instances built on them (site +-- `tensorObj_map_tmul`'s leg (c) pair), agree at `.default` … +example (X : Cᵒᵖ) : (↑(R.obj X) : Type u) = ↑((R ⋙ forget₂ CommRingCat RingCat).obj X) := rfl +example (X : Cᵒᵖ) : + (RingCat.instRingObjForgetRingHomCarrier (R := (R ⋙ forget₂ CommRingCat RingCat).obj X)) = + (CommRingCat.instCommRingObjForgetRingHomCarrier (R := R.obj X)).toRing := rfl +-- … but not at `.instances`/reducible, which is why leg (c) rejects the goal's candidate: +/-- +error: Tactic `rfl` failed: The left-hand side + RingCat.instRingObjForgetRingHomCarrier +is not definitionally equal to the right-hand side + CommRingCat.instCommRingObjForgetRingHomCarrier.toRing + +C : Type u_1 +inst✝ : Category.{v_1, u_1} C +R : Cᵒᵖ ⥤ CommRingCat +X : Cᵒᵖ +⊢ RingCat.instRingObjForgetRingHomCarrier = CommRingCat.instCommRingObjForgetRingHomCarrier.toRing +-/ +#guard_msgs in +example (X : Cᵒᵖ) : + (RingCat.instRingObjForgetRingHomCarrier (R := (R ⋙ forget₂ CommRingCat RingCat).obj X)) = + (CommRingCat.instCommRingObjForgetRingHomCarrier (R := R.obj X)).toRing := by + with_reducible_and_instances rfl + + + +-- Demo 3 (site `tensorObjMap`, leg (c) value pair). The smul the goal carries on the +-- `restrictScalars` object and the `ModuleCat`-native smul instance synthesis produces agree at +-- `.default` … +example {M₂ : PresheafOfModules.{u} (R ⋙ forget₂ _ _)} {X Y : Cᵒᵖ} (f : X ⟶ Y) : + (ModuleCat.instModuleCarrierObjRestrictScalars + (f := (R.map f).hom) (M := M₂.obj Y)).toDistribMulAction = + (M₂.obj Y).isModule.toDistribMulAction := rfl +-- … but not at `.instances`/reducible, so `CompatibleSMul.isScalarTower`'s `DistribMulAction` +-- slot rejects it: +set_option linter.style.longLine false in +/-- +error: Tactic `rfl` failed: The left-hand side + @Module.toDistribMulAction (↑(R.obj Y)) + (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y))) + CommRingCat.instCommRingObjForgetRingHomCarrier.toSemiring + ((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)).isAddCommGroup.toAddCommMonoid + ModuleCat.instModuleCarrierObjRestrictScalars +is not definitionally equal to the right-hand side + @Module.toDistribMulAction (↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)) (↑(M₂.obj Y)) + RingCat.instRingObjForgetRingHomCarrier.toSemiring (M₂.obj Y).isAddCommGroup.toAddCommMonoid (M₂.obj Y).isModule + +C : Type u_1 +inst✝ : Category.{v_1, u_1} C +R : Cᵒᵖ ⥤ CommRingCat +M₂ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat) +X Y : Cᵒᵖ +f : X ⟶ Y +⊢ ModuleCat.instModuleCarrierObjRestrictScalars.toDistribMulAction = (M₂.obj Y).isModule.toDistribMulAction +-/ +#guard_msgs in +example {M₂ : PresheafOfModules.{u} (R ⋙ forget₂ _ _)} {X Y : Cᵒᵖ} (f : X ⟶ Y) : + (ModuleCat.instModuleCarrierObjRestrictScalars + (f := (R.map f).hom) (M := M₂.obj Y)).toDistribMulAction = + (M₂.obj Y).isModule.toDistribMulAction := by + with_reducible rfl + +end PresheafOfModules.Monoidal +end InstanceTypesDemos + end PresheafOfModules diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Pushforward.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Pushforward.lean index 7f42f3237..3d4e9452b 100644 --- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Pushforward.lean +++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Pushforward.lean @@ -108,6 +108,9 @@ lemma pushforward_obj_map_apply (M : PresheafOfModules.{v} R) {X Y : Cᵒᵖ} (f (m : (ModuleCat.restrictScalars (φ.app X).hom).obj (M.obj (Opposite.op (F.obj X.unop)))) : (((pushforward φ).obj M).map f).hom m = M.map (F.map f.unop).op m := rfl +/-! # Issue (Low Severity) -/ + +set_option backward.isDefEq.instanceTypes "none" in set_option backward.isDefEq.respectTransparency.types false in /-- `@[simp]`-normal form of `pushforward_obj_map_apply`. -/ @[simp] @@ -118,10 +121,31 @@ lemma pushforward_obj_map_apply' (M : PresheafOfModules.{v} R) {X Y : Cᵒᵖ} ( ↑((ModuleCat.restrictScalars (S.map f).hom).obj ((ModuleCat.restrictScalars _).obj _))) (((pushforward φ).obj M).map f).hom m = M.map (F.map f.unop).op m := rfl +/-! +# Fix + +Add implicit-reducibility attrs, remove `respectTransparency.types false` +-/ + +attribute [local implicit_reducible] + pushforward + PresheafOfModules.restrictScalars PresheafOfModules.restrictScalarsObj +in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +example (M : PresheafOfModules.{v} R) {X Y : Cᵒᵖ} (f : X ⟶ Y) + (m : (ModuleCat.restrictScalars (φ.app X).hom).obj (M.obj (Opposite.op (F.obj X.unop)))) : + DFunLike.coe + (F := ↑((ModuleCat.restrictScalars _).obj _) →ₗ[_] + ↑((ModuleCat.restrictScalars (S.map f).hom).obj ((ModuleCat.restrictScalars _).obj _))) + (((pushforward φ).obj M).map f).hom m = M.map (F.map f.unop).op m := rfl + lemma pushforward_map_app_apply {M N : PresheafOfModules.{v} R} (α : M ⟶ N) (X : Cᵒᵖ) (m : (ModuleCat.restrictScalars (φ.app X).hom).obj (M.obj (Opposite.op (F.obj X.unop)))) : (((pushforward φ).map α).app X).hom m = α.app (Opposite.op (F.obj X.unop)) m := rfl +/-! # Issue 2 (Low Severity, same fix) -/ + +set_option backward.isDefEq.instanceTypes "none" in set_option backward.isDefEq.respectTransparency.types false in /-- `@[simp]`-normal form of `pushforward_map_app_apply`. -/ @[simp] @@ -131,6 +155,20 @@ lemma pushforward_map_app_apply' {M N : PresheafOfModules.{v} R} (α : M ⟶ N) (F := ↑((ModuleCat.restrictScalars _).obj _) →ₗ[_] ↑((ModuleCat.restrictScalars _).obj _)) (((pushforward φ).map α).app X).hom m = α.app (Opposite.op (F.obj X.unop)) m := rfl +/-! # Fix -/ + +attribute [local implicit_reducible] + pushforward + PresheafOfModules.restrictScalars PresheafOfModules.restrictScalarsObj +in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +/-- `@[simp]`-normal form of `pushforward_map_app_apply`. -/ +example {M N : PresheafOfModules.{v} R} (α : M ⟶ N) (X : Cᵒᵖ) + (m : (ModuleCat.restrictScalars (φ.app X).hom).obj (M.obj (Opposite.op (F.obj X.unop)))) : + DFunLike.coe + (F := ↑((ModuleCat.restrictScalars _).obj _) →ₗ[_] ↑((ModuleCat.restrictScalars _).obj _)) + (((pushforward φ).map α).app X).hom m = α.app (Opposite.op (F.obj X.unop)) m := rfl + section variable (R) in diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean index 6e1d44b59..ef8d7949f 100644 --- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean +++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean @@ -338,6 +338,9 @@ noncomputable def toSheafify : M₀ ⟶ (restrictScalars α).obj (sheafify α φ lemma toSheafify_app_apply (X : Cᵒᵖ) (x : M₀.obj X) : ((toSheafify α φ).app X).hom x = φ.app X x := rfl +/-! # Issue (Low Severity) -/ + +set_option backward.isDefEq.instanceTypes "none" in set_option backward.isDefEq.respectTransparency.types false in /-- `@[simp]`-normal form of `toSheafify_app_apply`. -/ @[simp] @@ -345,6 +348,19 @@ lemma toSheafify_app_apply' (X : Cᵒᵖ) (x : M₀.obj X) : DFunLike.coe (F := (_ →ₗ[_] ↑((ModuleCat.restrictScalars (α.app X).hom).obj _))) ((toSheafify α φ).app X).hom x = φ.app X x := rfl +/-! +# Fix + +implicit-reducible + respectTransparency.types +-/ + +attribute [local implicit_reducible] + PresheafOfModules.restrictScalars PresheafOfModules.restrictScalarsObj +in +example (X : Cᵒᵖ) (x : M₀.obj X) : + DFunLike.coe (F := (_ →ₗ[_] ↑((ModuleCat.restrictScalars (α.app X).hom).obj _))) + ((toSheafify α φ).app X).hom x = φ.app X x := rfl + @[simp] lemma toPresheaf_map_toSheafify : (toPresheaf R₀).map (toSheafify α φ) = φ := rfl diff --git a/mathlib4/Mathlib/Algebra/Group/Hom/Defs.lean b/mathlib4/Mathlib/Algebra/Group/Hom/Defs.lean index 5aa3b8cc6..0284322a8 100644 --- a/mathlib4/Mathlib/Algebra/Group/Hom/Defs.lean +++ b/mathlib4/Mathlib/Algebra/Group/Hom/Defs.lean @@ -259,7 +259,7 @@ theorem ne_one_of_map {R S F : Type*} [One R] [One S] [FunLike F R S] [OneHomCla /-- Turn an element of a type `F` satisfying `OneHomClass F M N` into an actual `OneHom`. This is declared as the default coercion from `F` to `OneHom M N`. -/ -@[to_additive (attr := coe) +@[to_additive (attr := coe, instance_reducible) /-- Turn an element of a type `F` satisfying `ZeroHomClass F M N` into an actual `ZeroHom`. This is declared as the default coercion from `F` to `ZeroHom M N`. -/] def OneHomClass.toOneHom [OneHomClass F M N] (f : F) : OneHom M N where @@ -332,7 +332,7 @@ lemma map_comp_mul [MulHomClass F M N] (f : F) (g h : ι → M) : f ∘ (g * h) /-- Turn an element of a type `F` satisfying `MulHomClass F M N` into an actual `MulHom`. This is declared as the default coercion from `F` to `M →ₙ* N`. -/ -@[to_additive (attr := coe) +@[to_additive (attr := coe, instance_reducible) /-- Turn an element of a type `F` satisfying `AddHomClass F M N` into an actual `AddHom`. This is declared as the default coercion from `F` to `M →ₙ+ N`. -/] def MulHomClass.toMulHom [MulHomClass F M N] (f : F) : M →ₙ* N where @@ -400,7 +400,7 @@ variable [FunLike F M N] /-- Turn an element of a type `F` satisfying `MonoidHomClass F M N` into an actual `MonoidHom`. This is declared as the default coercion from `F` to `M →* N`. -/ -@[to_additive (attr := coe) +@[to_additive (attr := coe, instance_reducible) /-- Turn an element of a type `F` satisfying `AddMonoidHomClass F M N` into an actual `MonoidHom`. This is declared as the default coercion from `F` to `M →+ N`. -/] def MonoidHomClass.toMonoidHom [MonoidHomClass F M N] (f : F) : M →* N := diff --git a/mathlib4/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean b/mathlib4/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean index d7dba586b..ffd5bab70 100644 --- a/mathlib4/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean +++ b/mathlib4/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.Homology.HomotopyCategory.HomComplex public import Mathlib.Algebra.Homology.HomotopyCategory.Shift public import Mathlib.Algebra.Module.Equiv.Basic public import Mathlib.Tactic.Linarith +meta import Lean.PostprocessTraces /-! # Shifting cochains @@ -292,7 +293,13 @@ lemma rightShift_smul (a n' : ℤ) (hn' : n' + a = n) (x : R) : dsimp simp only [rightShift_v _ a n' hn' p q hpq _ rfl, smul_v, Linear.smul_comp] -set_option backward.isDefEq.respectTransparency false in +/-! # Issue -/ + +-- fixed by making `shiftFunctor` implicit-reducible, so that `respectTransparency types` +-- can be removed +set_option allowUnsafeReducibility true +attribute [local implicit_reducible] shiftFunctor in +set_option backward.isDefEq.instanceTypes "markOrSynth" in @[simp] lemma leftShift_smul (a n' : ℤ) (hn' : n + a = n') (x : R) : (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn' := by @@ -301,6 +308,137 @@ lemma leftShift_smul (a n' : ℤ) (hn' : n + a = n') (x : R) : simp only [leftShift_v _ a n' hn' p q hpq (p + a) (by lia), smul_v, Linear.comp_smul, smul_comm x] +/-! ## Explanation -/ + +open Lean.PostprocessTraces + +/-- Truncate every trace subtree below `depth`. -/ +private meta partial def maxDepth (depth : Nat) : TracePostprocessor := fun trees => + let rec truncateTree (t : TraceTree) (depth : Nat) : TraceTree := + match t with + | .leaf msg => TraceTree.leaf msg + | .node data msg children wrap => + match depth with + | 0 => .node data m!"{msg} (truncated)" #[] wrap + | depth' + 1 => .node data msg (children.map (truncateTree · depth')) wrap + return trees.map (truncateTree · depth) + +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +-- The dual of `filterSubtrees`: drop matching subtrees (used to remove `onFailure` duplicates). +private meta partial def dropSubtrees (p : TracePattern) : TracePostprocessor := + fun trees => trees.filterMapM go +where + go (t : TraceTree) : Lean.CoreM (Option TraceTree) := do + if ← p t then + return none + match t with + | .leaf msg => return some (.leaf msg) + | .node data msg children wrap => return some (.node data msg (← children.filterMapM go) wrap) + +-- Without the `implicit_reducible shiftFunctor` lever the closing `simp only` fails. `leftShift` +-- carries a sign `u : ℤˣ`, so `simp` fires `smul_comm x`, forcing synthesis of +-- `SMulCommClass R ℤˣ (K.X (p + a) ⟶ L.X q)`. The only candidate `Units.smulCommClass_right` must +-- reproduce its `SMul R _` argument, and unifying its conclusion assigns that mvar the goal's +-- shift-spelled `SMul R (((shiftFunctor …).obj K).X p ⟶ L.X q)`. The direct `.instances` type +-- check against the mvar's `SMul R (K.X (p + a) ⟶ L.X q)` fails (the semireducible shift functor +-- does not unfold there); under `markOrSynth` the fallback synthesizes the mvar's own type +-- (`✅ … (truncated)`) but the candidate is still not defeq to it at `.instances`, so the +-- assignment is rejected, `SMulCommClass` is unsynthesizable, `smul_comm x` never fires and the +-- goal `u • x • f = x • u • f` is left unsolved. +set_option linter.style.longLine false in +set_option linter.unusedSimpArgs false in +/-- +error: unsolved goals +C : Type u +inst✝³ : Category.{v, u} C +inst✝² : Preadditive C +R : Type u_1 +inst✝¹ : Ring R +inst✝ : Linear R C +K L M : CochainComplex C ℤ +n : ℤ +γ γ₁ γ₂ : Cochain K L n +a n' : ℤ +hn' : n + a = n' +x : R +p q : ℤ +hpq : p + n' = q +⊢ (a * n' + a * (a - 1) / 2).negOnePow • x • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) q ⋯ = + x • (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) q ⋯ +--- +trace: [Meta.synthInstance] ❌️ SMulCommClass R ℤˣ (K.X (p + a) ⟶ L.X q) + [Meta.synthInstance.apply] ❌️ apply @Units.smulCommClass_right to SMulCommClass R ℤˣ (K.X (p + a) ⟶ L.X q) + [Meta.synthInstance.tryResolve] ❌️ SMulCommClass R ℤˣ (K.X (p + a) ⟶ L.X q) ≟ SMulCommClass ?m.77 ?m.78ˣ ?m.79 + [Meta.isDefEq] ❌️ [instances] SMulCommClass R ℤˣ (K.X (p + a) ⟶ L.X q) =?= SMulCommClass ?m.77 ?m.78ˣ ?m.79 + [Meta.isDefEq] ❌️ [instances] DistribMulAction.toDistribSMul.toSMul =?= ?m.81 + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.81 : SMul R + (K.X (p + a) ⟶ + L.X + q)) := (DistribMulAction.toDistribSMul.toSMul : SMul R + (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).X p ⟶ L.X q)) + [Meta.isDefEq] ❌️ [instances] SMul R + (K.X (p + a) ⟶ + L.X q) =?= SMul R (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).X p ⟶ L.X q) + [Meta.isDefEq] ✅️ [instances] R =?= R (truncated) + [Meta.isDefEq] ❌️ [instances] K.X (p + a) ⟶ + L.X q =?= ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).X p ⟶ L.X q (truncated) + [Meta.synthInstance] ✅️ SMul R (K.X (p + a) ⟶ L.X q) (truncated) + [Meta.isDefEq] ❌️ [instances] DistribMulAction.toDistribSMul.toSMul =?= DistribMulAction.toDistribSMul.toSMul + [Meta.isDefEq] ❌️ [instances] DistribMulAction.toDistribSMul.toSMulZeroClass.1 =?= DistribMulAction.toDistribSMul.toSMulZeroClass.1 (truncated) + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.81 : SMul R + (K.X (p + a) ⟶ + L.X + q)) := ((Linear.homModule (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).X p) + (L.X + q)).toSemigroupAction.1 : SMul R + (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).X p ⟶ L.X q)) + [Meta.isDefEq] ❌️ [instances] SMul R + (K.X (p + a) ⟶ + L.X q) =?= SMul R (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).X p ⟶ L.X q) + [Meta.isDefEq] ✅️ [instances] R =?= R (truncated) + [Meta.isDefEq] ❌️ [instances] K.X (p + a) ⟶ + L.X q =?= ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).X p ⟶ L.X q (truncated) + [Meta.synthInstance] ✅️ SMul R (K.X (p + a) ⟶ L.X q) (truncated) + [Meta.isDefEq] ❌️ [instances] (Linear.homModule + (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).X p) + (L.X q)).toSemigroupAction.1 =?= DistribMulAction.toDistribSMul.toSMul + [Meta.isDefEq] ❌️ [instances] (Linear.homModule + (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).X p) + (L.X q)).toSemigroupAction.1 =?= DistribMulAction.toDistribSMul.toSMulZeroClass.1 (truncated) +-/ +#guard_msgs in +set_option trace.Meta.synthInstance true in +set_option trace.Meta.isDefEq true in +set_option trace.Meta.isDefEq.printTransparency true in +set_option trace.Meta.isDefEq.assign.checkTypes true in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option backward.isDefEq.respectTransparency false in +postprocess_traces + filterSubtrees (fun x => (ofClass `Meta.synthInstance.apply x) + <&&> (containsString "smulCommClass_right" x) <&&> failed x) + >=> filterSubtrees (fun x => (ofClass `Meta.isDefEq.assign.checkTypes x) <&&> failed x) + >=> maxDepth 7 + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> succeeded x) + >=> dropSubtrees (fun x => ofClass `Meta.isDefEq.onFailure x) +in +example (a n' : ℤ) (hn' : n + a = n') (x : R) : + (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn' := by + ext p q hpq + dsimp + simp only [leftShift_v _ a n' hn' p q hpq (p + a) (by lia), smul_v, Linear.comp_smul, + smul_comm x] + set_option backward.isDefEq.respectTransparency false in @[simp] lemma shift_smul (a : ℤ) (x : R) : diff --git a/mathlib4/Mathlib/Algebra/Lie/BaseChange.lean b/mathlib4/Mathlib/Algebra/Lie/BaseChange.lean index 75dd94397..db685f328 100644 --- a/mathlib4/Mathlib/Algebra/Lie/BaseChange.lean +++ b/mathlib4/Mathlib/Algebra/Lie/BaseChange.lean @@ -8,6 +8,8 @@ module public import Mathlib.Algebra.Algebra.RestrictScalars public import Mathlib.Algebra.Lie.TensorProduct +meta import Lean.PostprocessTraces + /-! # Extension and restriction of scalars for Lie algebras and Lie modules @@ -25,6 +27,8 @@ scalars. lie ring, lie algebra, extension of scalars, restriction of scalars, base change -/ +open Lean.PostprocessTraces + @[expose] public section open scoped TensorProduct @@ -149,7 +153,6 @@ end ExtendScalars namespace RestrictScalars - variable [h : LieRing L] instance : LieRing (RestrictScalars R A L) := @@ -157,11 +160,93 @@ instance : LieRing (RestrictScalars R A L) := variable [CommRing A] [LieAlgebra A L] +/-! # Issue -/ + +set_option backward.isDefEq.instanceTypes "markOrSynth" in set_option backward.isDefEq.respectTransparency false in instance lieAlgebra [CommRing R] [Algebra R A] : LieAlgebra R (RestrictScalars R A L) where lie_smul t x y := (lie_smul (algebraMap R A t) (RestrictScalars.addEquiv R A L x) (RestrictScalars.addEquiv R A L y) :) +/-! ## Explanation -/ + +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +-- The dual of `filterSubtrees`: drop matching subtrees (used to remove `onFailure` duplicates). +private meta partial def dropSubtrees (p : TracePattern) : TracePostprocessor := + fun trees => trees.filterMapM go +where + go (t : TraceTree) : Lean.CoreM (Option TraceTree) := do + if ← p t then + return none + match t with + | .leaf msg => return some (.leaf msg) + | .node data msg children wrap => return some (.node data msg (← children.filterMapM go) wrap) + +-- `RestrictScalars R A L := L` is a semireducible synonym carrying a *different* `Module R` +-- structure. Synthesizing the `Module R (RestrictScalars R A L)` parent of `LieAlgebra` via +-- `RestrictScalars.module` assigns its `AddCommMonoid` argument across the synonym: the direct +-- `.instances` type check `AddCommMonoid L =?= AddCommMonoid (RestrictScalars R A L)` fails (the +-- synonym does not unfold there). Under `markOrSynth` the fallback synthesizes the mvar's own +-- type (`✅ AddCommMonoid L`) and unifies the candidate with it at `.default`, which succeeds and +-- rescues the assignment. Under plain `mark` there is no fallback and the structure elaborator +-- reports `Fields missing: add_smul, zero_smul`. +set_option linter.style.longLine false in +/-- +trace: [Meta.synthInstance] ✅️ Module R (RestrictScalars R A L) + [Meta.synthInstance.apply] ✅️ apply RestrictScalars.module to Module R (RestrictScalars R A L) + [Meta.synthInstance.tryResolve] ✅️ Module R (RestrictScalars R A L) ≟ Module R (RestrictScalars R A L) + [Meta.isDefEq] ✅️ [instances] Module R + (RestrictScalars R A L) =?= Module ?m.12 (RestrictScalars ?m.12 ?m.13 ?m.14) + [Meta.isDefEq] ✅️ [default] (instLieRingRestrictScalars R A + L).toAddCommMonoid =?= instAddCommMonoidRestrictScalars R A L + [Meta.isDefEq] ✅️ [default] { toAddMonoid := (instLieRingRestrictScalars R A L).toAddMonoid, + add_comm := ⋯ } =?= ?m.16 + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.16 : AddCommMonoid + L) := ({ toAddMonoid := (instLieRingRestrictScalars R A L).toAddMonoid, + add_comm := ⋯ } : AddCommMonoid (RestrictScalars R A L)) + [Meta.isDefEq] ❌️ [instances] AddCommMonoid L =?= AddCommMonoid (RestrictScalars R A L) + [Meta.isDefEq] ❌️ [instances] L =?= RestrictScalars R A L + [Meta.synthInstance] ✅️ AddCommMonoid L (truncated) + [Meta.isDefEq] ✅️ [default] { toAddMonoid := (instLieRingRestrictScalars R A L).toAddMonoid, + add_comm := ⋯ } =?= h.toAddCommMonoid (truncated) +--- +warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended for development and not for final code. If you intend to submit this contribution to the Mathlib project, please remove 'set_option trace.Meta.isDefEq'. + +Note: This linter can be disabled with `set_option linter.style.setOption false` +-/ +#guard_msgs in +postprocess_traces + filterSubtrees (fun x => (ofClass `Meta.synthInstance.apply x) <&&> + (containsString "RestrictScalars.module" x)) + >=> filterSubtrees (fun x => (ofClass `Meta.isDefEq.assign.checkTypes x) <&&> + (containsString "AddCommMonoid" x)) + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> succeeded x <&&> + containsString "AddCommMonoid L" x) + >=> elideBelow (fun x => (ofClass `Meta.isDefEq x) <&&> succeeded x <&&> + containsString "h.toAddCommMonoid" x) + >=> dropSubtrees (fun x => ofClass `Meta.isDefEq.onFailure x) +in +set_option trace.Meta.isDefEq true in +set_option trace.Meta.isDefEq.printTransparency true in +set_option trace.Meta.isDefEq.assign.checkTypes true in +set_option trace.Meta.synthInstance true in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option backward.isDefEq.respectTransparency false in +example [CommRing R] [Algebra R A] : LieAlgebra R (RestrictScalars R A L) where + lie_smul t x y := (lie_smul (algebraMap R A t) (RestrictScalars.addEquiv R A L x) + (RestrictScalars.addEquiv R A L y) :) + end RestrictScalars end LieAlgebra diff --git a/mathlib4/Mathlib/Algebra/Module/Equiv/Defs.lean b/mathlib4/Mathlib/Algebra/Module/Equiv/Defs.lean index 14a412f25..146785c8a 100644 --- a/mathlib4/Mathlib/Algebra/Module/Equiv/Defs.lean +++ b/mathlib4/Mathlib/Algebra/Module/Equiv/Defs.lean @@ -7,6 +7,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne module public import Mathlib.Algebra.Module.LinearMap.Defs +meta import Lean.PostprocessTraces /-! # (Semi)linear equivalences @@ -584,11 +585,125 @@ def _root_.RingEquiv.toSemilinearEquiv (f : R ≃+* S) : toFun := f map_smul' := f.map_mul } +open Lean.PostprocessTraces + +/-! # Issue -/ + set_option backward.isDefEq.respectTransparency false in +-- Verdict: Rightly fails if we enforce the type at instance transparency. +set_option backward.isDefEq.instanceTypes "none" in @[simp] lemma _root_.RingEquiv.symm_toSemilinearEquiv_symm_apply (f : R ≃+* S) (x : R) : f.symm.toSemilinearEquiv.symm (σ' := RingHomClass.toRingHom f) x = f x := rfl +/-! +## Explanation + +"markOrSynth": + +`RingInvHomPair` instance cannot be unified because types don't match at instances (`.symm.symm`), +and it can't be synthesized either. +-/ + +example (f : R ≃+* S) : (↑f : R →+* S) = ↑f.symm.symm := by rfl + +open Lean.PostprocessTraces + +/-- +error: Function expected at + f.symm.toSemilinearEquiv.symm +but this term has type + R ≃ₛₗ[↑f] S + +Note: Expected a function because this term is being applied to the argument + x +--- +trace: [Meta.synthInstance] ❌️ CoeFun (R ≃ₛₗ[↑f] S) ?m.35 + [Meta.synthInstance.apply] ❌️ apply @instEquivLike to EquivLike (R ≃ₛₗ[↑f] S) ?m.43 ?m.44 + [Meta.synthInstance.tryResolve] ❌️ EquivLike (R ≃ₛₗ[↑f] S) ?m.43 + ?m.44 ≟ EquivLike (?m.48 ≃ₛₗ[?m.56] ?m.49) ?m.48 ?m.49 + [Meta.isDefEq] ❌️ [instances] EquivLike (R ≃ₛₗ[↑f] S) ?m.43 + ?m.44 =?= EquivLike (?m.48 ≃ₛₗ[?m.56] ?m.49) ?m.48 ?m.49 + [Meta.isDefEq] ❌️ [instances] R ≃ₛₗ[↑f] S =?= ?m.48 ≃ₛₗ[?m.56] ?m.49 + [Meta.isDefEq.transparency] raising transparency instances → implicit + [Meta.isDefEq] ✅️ [implicit] R =?= ?m.46 + [Meta.isDefEq] R [nonassignable] =?= ?m.46 [assignable] + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.46 : Type ?u.43) := (R : Type u_1) + [Meta.isDefEq] ✅️ [implicit] Type ?u.43 =?= Type u_1 + [Meta.isDefEq.transparency] raising transparency instances → implicit + [Meta.isDefEq] ✅️ [implicit] S =?= ?m.47 + [Meta.isDefEq] S [nonassignable] =?= ?m.47 [assignable] + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.47 : Type ?u.44) := (S : Type u_6) + [Meta.isDefEq] ✅️ [implicit] Type ?u.44 =?= Type u_6 + [Meta.isDefEq.transparency] raising transparency instances → implicit + [Meta.isDefEq] ✅️ [implicit] inst✝¹ =?= ?m.50 + [Meta.isDefEq] inst✝¹ [nonassignable] =?= ?m.50 [assignable] + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.50 : Semiring R) := (inst✝¹ : Semiring R) + [Meta.isDefEq] ✅️ [instances] Semiring R =?= Semiring R + [Meta.isDefEq] ✅️ [instances] R =?= R + [Meta.isDefEq.transparency] raising transparency instances → implicit + [Meta.isDefEq] ✅️ [implicit] inst✝ =?= ?m.51 + [Meta.isDefEq] inst✝ [nonassignable] =?= ?m.51 [assignable] + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.51 : Semiring S) := (inst✝ : Semiring S) + [Meta.isDefEq] ✅️ [instances] Semiring S =?= Semiring S + [Meta.isDefEq] ✅️ [instances] S =?= S + [Meta.isDefEq] ✅️ [instances] ↑f =?= ?m.56 + [Meta.isDefEq] ↑f [nonassignable] =?= ?m.56 [assignable] + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.56 : R →+* S) := (↑f : R →+* S) + [Meta.isDefEq.transparency] raising transparency instances → implicit + [Meta.isDefEq] ✅️ [implicit] R →+* S =?= R →+* S + [Meta.isDefEq] ✅️ [implicit] R =?= R + [Meta.isDefEq] ✅️ [implicit] S =?= S + [Meta.isDefEq] ✅️ [implicit] inst✝¹.toNonAssocSemiring =?= inst✝¹.toNonAssocSemiring + [Meta.isDefEq] ✅️ [implicit] inst✝.toNonAssocSemiring =?= inst✝.toNonAssocSemiring + [Meta.isDefEq.transparency] raising transparency instances → implicit + [Meta.isDefEq] ✅️ [implicit] ↑f.symm =?= ?m.57 + [Meta.isDefEq] ↑f.symm [nonassignable] =?= ?m.57 [assignable] + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.57 : S →+* R) := (↑f.symm : S →+* R) + [Meta.isDefEq] ✅️ [implicit] S →+* R =?= S →+* R + [Meta.isDefEq] ✅️ [implicit] S =?= S + [Meta.isDefEq] ✅️ [implicit] R =?= R + [Meta.isDefEq] ✅️ [implicit] inst✝.toNonAssocSemiring =?= inst✝.toNonAssocSemiring + [Meta.isDefEq] ✅️ [implicit] inst✝¹.toNonAssocSemiring =?= inst✝¹.toNonAssocSemiring + [Meta.isDefEq.transparency] raising transparency instances → implicit + [Meta.isDefEq] ❌️ [implicit] RingHomInvPair.symm ↑f.symm ↑f.symm.symm =?= ?m.58 + [Meta.isDefEq] RingHomInvPair.symm ↑f.symm ↑f.symm.symm [nonassignable] =?= ?m.58 [assignable] + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.58 : RingHomInvPair ↑f + ↑f.symm) := (RingHomInvPair.symm ↑f.symm ↑f.symm.symm : RingHomInvPair ↑f.symm.symm ↑f.symm) + [Meta.isDefEq] ❌️ [instances] RingHomInvPair ↑f ↑f.symm =?= RingHomInvPair ↑f.symm.symm ↑f.symm + [Meta.isDefEq] ❌️ [instances] ↑f =?= ↑f.symm.symm + [Meta.isDefEq] ❌️ [instances] f =?= f.symm.symm + [Meta.isDefEq.onFailure] ❌️ f =?= f.symm.symm + [Meta.isDefEq.onFailure] ❌️ ↑f =?= ↑f.symm.symm + [Meta.isDefEq.onFailure] ❌️ RingHomInvPair ↑f ↑f.symm =?= RingHomInvPair ↑f.symm.symm ↑f.symm + [Meta.synthInstance] ❌️ RingHomInvPair ↑f ↑f.symm + [Meta.synthInstance] ✅️ no instances for RingHomInvPair (↑f) _tc.0 + [Meta.synthInstance.instances] #[] + [Meta.synthInstance] result + [Meta.isDefEq.onFailure] ❌️ R ≃ₛₗ[↑f] S =?= ?m.48 ≃ₛₗ[?m.56] ?m.49 + [Meta.isDefEq.onFailure] ❌️ EquivLike (R ≃ₛₗ[↑f] S) ?m.43 + ?m.44 =?= EquivLike (?m.48 ≃ₛₗ[?m.56] ?m.49) ?m.48 ?m.49 +-/ +#guard_msgs in +postprocess_traces + filterSubtrees (fun x => (ofClass `Meta.synthInstance.apply x) + <&&> (containsString "LinearEquiv.instEquivLike" x)) +in +attribute [local implicit_reducible] + MulEquiv.symm + RingEquiv.symm in +set_option trace.Meta.isDefEq true in +set_option trace.Meta.isDefEq.printTransparency true in +set_option trace.Meta.synthInstance true in +set_option trace.Meta.isDefEq.assign.checkTypes true in +-- set_option backward.isDefEq.respectTransparency false in +-- Verdict: Rightly fails if we enforce the type at instance transparency. +set_option backward.isDefEq.instanceTypes "markOrSynth" in +@[simp] +example (f : R ≃+* S) (x : R) : + f.symm.toSemilinearEquiv.symm (σ' := RingHomClass.toRingHom f) x = f x := by + rfl + variable [AddCommMonoid M] /-- An involutive linear map is a linear equivalence. -/ diff --git a/mathlib4/Mathlib/Algebra/Module/LinearMap/Index.lean b/mathlib4/Mathlib/Algebra/Module/LinearMap/Index.lean index 8da65af7f..ad2d4deb0 100644 --- a/mathlib4/Mathlib/Algebra/Module/LinearMap/Index.lean +++ b/mathlib4/Mathlib/Algebra/Module/LinearMap/Index.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.Exact.Sequence public import Mathlib.Algebra.Module.LinearMap.Defs public import Mathlib.Algebra.Module.Submodule.Map public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas +meta import Lean.PostprocessTraces /-! # The index of a linear map @@ -65,13 +66,124 @@ public lemma index_of_surjective (hf : Surjective f) : rw [index_eq_finrank_sub, range_eq_top.mpr hf] simp [finrank_eq_zero_of_subsingleton] -set_option backward.isDefEq.respectTransparency.types false in +/-! # Issue -/ + +set_option allowUnsafeReducibility true in +attribute [local implicit_reducible] ker in +set_option backward.isDefEq.instanceTypes "markOrSynth" in @[simp] public lemma index_id : (id : M →ₗ[R] M).index = 0 := by nontriviality R rw [index_eq_finrank_sub, range_id] simp [finrank_eq_zero_of_subsingleton] +/-! ## Explanation -/ + +open Lean.PostprocessTraces + +/-- Truncate every trace subtree below `depth`. -/ +private meta partial def maxDepth (depth : Nat) : TracePostprocessor := fun trees => + let rec truncateTree (t : TraceTree) (depth : Nat) : TraceTree := + match t with + | .leaf msg => TraceTree.leaf msg + | .node data msg children wrap => + match depth with + | 0 => .node data m!"{msg} (truncated)" #[] wrap + | depth' + 1 => .node data msg (children.map (truncateTree · depth')) wrap + return trees.map (truncateTree · depth) + +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +-- The dual of `filterSubtrees`: drop matching subtrees (used to remove `onFailure` duplicates). +private meta partial def dropSubtrees (p : TracePattern) : TracePostprocessor := + fun trees => trees.filterMapM go +where + go (t : TraceTree) : Lean.CoreM (Option TraceTree) := do + if ← p t then + return none + match t with + | .leaf msg => return some (.leaf msg) + | .node data msg children wrap => return some (.node data msg (← children.filterMapM go) wrap) + +-- Without the `implicit_reducible ker` lever the closing `simp` fails. After `range_id`, the +-- `@[simp]` `rfl`-lemma `ker_id` rewrites the carrier `↥(ker id)` to `↥⊥` but simp keeps the old +-- `id.ker.*` instance arguments; discharging `Module.Free R ↥⊥` (needed by +-- `finrank_eq_zero_of_subsingleton`) then tries `Free.of_subsingleton`, which assigns the +-- inherited `id.ker.addCommMonoid` to its `AddCommMonoid ↥⊥` mvar. The direct `.instances` check +-- `AddCommMonoid ↥⊥ =?= AddCommMonoid ↥id.ker` fails (neither `ker` nor `id` unfolds there); +-- under `markOrSynth` the fallback synthesizes `↥⊥`'s own `AddCommMonoid` (`✅ … (truncated)`) but +-- the candidate is still not defeq to it at `.instances`, so the assignment is rejected, `Free` +-- is unsynthesizable, `finrank R ↥⊥` is left unrewritten and `simp` fails to close the goal. +set_option linter.style.longLine false in +/-- +error: unsolved goals +M : Type u_1 +N : Type u_2 +inst✝⁵ : AddCommGroup M +inst✝⁴ : AddCommGroup N +R : Type u_3 +inst✝³ : Ring R +inst✝² : Module R M +inst✝¹ : Module R N +f : M →ₗ[R] N +inst✝ : StrongRankCondition R +a✝ : Nontrivial R +⊢ finrank R ↥⊥ = 0 +--- +trace: [Meta.synthInstance] ❌️ Free R ↥⊥ + [Meta.synthInstance.apply] ❌️ apply Free.of_subsingleton to Free R ↥⊥ + [Meta.synthInstance.tryResolve] ❌️ Free R ↥⊥ ≟ Free ?m.72 ?m.73 + [Meta.isDefEq] ❌️ [instances] Free R ↥⊥ =?= Free ?m.72 ?m.73 + [Meta.isDefEq] ❌️ [implicit] id.ker.addCommMonoid =?= ?m.75 + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.75 : AddCommMonoid + ↥⊥) := (id.ker.addCommMonoid : AddCommMonoid ↥id.ker) + [Meta.isDefEq] ❌️ [instances] AddCommMonoid ↥⊥ =?= AddCommMonoid ↥id.ker + [Meta.isDefEq] ❌️ [instances] ↥⊥ =?= ↥id.ker (truncated) + [Meta.synthInstance] ✅️ AddCommMonoid ↥⊥ (truncated) + [Meta.isDefEq] ❌️ [implicit] id.ker.addCommMonoid =?= ⊥.addCommMonoid + [Meta.isDefEq] ❌️ [implicit] id.ker =?= ⊥ (truncated) + [Meta.isDefEq] ❌️ [implicit] AddSubmonoidClass.toAddCommMonoid + id.ker =?= AddSubmonoidClass.toAddCommMonoid ⊥ (truncated) + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.75 : AddCommMonoid + ↥⊥) := ({ toAddMonoid := AddSubmonoidClass.toAddMonoid id.ker, add_comm := ⋯ } : AddCommMonoid ↥id.ker) + [Meta.isDefEq] ❌️ [instances] AddCommMonoid ↥⊥ =?= AddCommMonoid ↥id.ker + [Meta.isDefEq] ❌️ [instances] ↥⊥ =?= ↥id.ker (truncated) + [Meta.synthInstance] ✅️ AddCommMonoid ↥⊥ (truncated) + [Meta.isDefEq] ❌️ [implicit] { toAddMonoid := AddSubmonoidClass.toAddMonoid id.ker, + add_comm := ⋯ } =?= ⊥.addCommMonoid + [Meta.isDefEq] ❌️ [implicit] { toAddMonoid := AddSubmonoidClass.toAddMonoid id.ker, + add_comm := ⋯ } =?= AddSubmonoidClass.toAddCommMonoid ⊥ (truncated) +-/ +#guard_msgs in +set_option trace.Meta.synthInstance true in +set_option trace.Meta.isDefEq true in +set_option trace.Meta.isDefEq.printTransparency true in +set_option trace.Meta.isDefEq.assign.checkTypes true in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option backward.isDefEq.respectTransparency.types false in +postprocess_traces + filterSubtrees (fun x => (ofClass `Meta.synthInstance.apply x) + <&&> (containsString "Free.of_subsingleton" x) <&&> failed x) + >=> filterSubtrees (fun x => (ofClass `Meta.isDefEq.assign.checkTypes x) <&&> failed x) + >=> maxDepth 7 + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> succeeded x) + >=> dropSubtrees (fun x => ofClass `Meta.isDefEq.onFailure x) +in +example : (id : M →ₗ[R] M).index = 0 := by + nontriviality R + rw [index_eq_finrank_sub, range_id] + simp [finrank_eq_zero_of_subsingleton] + @[simp] public lemma _root_.LinearEquiv.index_eq_zero {e : M ≃ₗ[R] N} : e.toLinearMap.index = 0 := by nontriviality R diff --git a/mathlib4/Mathlib/Algebra/Module/Presentation/Differentials.lean b/mathlib4/Mathlib/Algebra/Module/Presentation/Differentials.lean index 97d84e50e..7099046f8 100644 --- a/mathlib4/Mathlib/Algebra/Module/Presentation/Differentials.lean +++ b/mathlib4/Mathlib/Algebra/Module/Presentation/Differentials.lean @@ -84,6 +84,13 @@ lemma hom₁_single (r : σ) : hom₁ pres (Finsupp.single r 1) = Extension.Cotangent.mk ⟨pres.relation r, by simp⟩ := by simp [hom₁] +/-! +# Issue (Low Severity) + +Fixed by making `Generators.toExtension` implicit-reducible and removing `respectTransparency false` +-/ + +set_option backward.isDefEq.instanceTypes "none" in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma surjective_hom₁ : Function.Surjective (hom₁ pres) := by @@ -112,6 +119,37 @@ lemma surjective_hom₁ : Function.Surjective (hom₁ pres) := by simp only [LinearMap.coe_mk, AddHom.coe_mk, hom₁_single, φ] rfl +/-! +# Fix +-/ + +attribute [local implicit_reducible] Generators.toExtension in +set_option backward.defeqAttrib.useBackward true in +example : Function.Surjective (hom₁ pres) := by + let φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := + { toFun := hom₁ pres + map_add' := by simp + map_smul' := by simp } + change Function.Surjective φ + have h₁ := Algebra.Extension.Cotangent.mk_surjective (P := pres.toExtension) + have h₂ : Submodule.span pres.Ring + (Set.range (fun r ↦ (⟨pres.relation r, by simp⟩ : pres.ker))) = ⊤ := by + refine Submodule.map_injective_of_injective (f := Submodule.subtype pres.ker) + Subtype.coe_injective ?_ + rw [Submodule.map_top, Submodule.range_subtype, Submodule.map_span, + Submodule.coe_subtype, Ideal.submodule_span_eq] + simp only [← pres.span_range_relation_eq_ker] + congr + aesop + rw [← LinearMap.range_eq_top] at h₁ ⊢ + rw [← top_le_iff, ← h₁, LinearMap.range_eq_map, ← h₂] + dsimp + rw [Submodule.map_span_le] + rintro _ ⟨r, rfl⟩ + simp only [LinearMap.mem_range] + refine ⟨Finsupp.single r 1, ?_⟩ + simp only [LinearMap.coe_mk, AddHom.coe_mk, hom₁_single, φ] + set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma comm₁₂_single (r : σ) : diff --git a/mathlib4/Mathlib/Algebra/Order/Archimedean/Basic.lean b/mathlib4/Mathlib/Algebra/Order/Archimedean/Basic.lean index 739a8386b..ace23f99c 100644 --- a/mathlib4/Mathlib/Algebra/Order/Archimedean/Basic.lean +++ b/mathlib4/Mathlib/Algebra/Order/Archimedean/Basic.lean @@ -57,6 +57,7 @@ instance OrderDual.instMulArchimedean [CommGroup G] [PartialOrder G] [IsOrderedM let ⟨n, hn⟩ := MulArchimedean.arch (ofDual x)⁻¹ (one_lt_inv'.2 hy) ⟨n, by rwa [inv_pow, inv_le_inv_iff] at hn⟩⟩ +-- attribute [local instance] Additive.partialOrderAdditiveToPartialOrder in instance Additive.instArchimedean [CommGroup G] [PartialOrder G] [MulArchimedean G] : Archimedean (Additive G) := ⟨fun x _ hy ↦ MulArchimedean.arch x.toMul hy⟩ diff --git a/mathlib4/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean b/mathlib4/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean index 72e1b6508..ce4836e7a 100644 --- a/mathlib4/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean +++ b/mathlib4/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean @@ -98,6 +98,7 @@ instance instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual : top_add' a := by ext; simp [bot_eq_zero] isAddLeftRegular_of_ne_top := by simp +contextual [IsRegular.of_ne_zero, bot_eq_zero] + set_option backward.isDefEq.respectTransparency false in instance instLinearOrderedAddCommMonoidWithTopOrderDualAdditive : LinearOrderedAddCommMonoidWithTop (Additive α)ᵒᵈ where diff --git a/mathlib4/Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean b/mathlib4/Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean index f34785986..30c3d12fe 100644 --- a/mathlib4/Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean +++ b/mathlib4/Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean @@ -15,6 +15,9 @@ public section variable {α : Type*} +set_option allowUnsafeReducibility true +-- attribute [implicit_reducible] Additive Multiplicative + instance [LE α] : LE (Multiplicative α) := inferInstanceAs <| LE α diff --git a/mathlib4/Mathlib/AlgebraicGeometry/Limits.lean b/mathlib4/Mathlib/AlgebraicGeometry/Limits.lean index fe1f9c51d..492b78efe 100644 --- a/mathlib4/Mathlib/AlgebraicGeometry/Limits.lean +++ b/mathlib4/Mathlib/AlgebraicGeometry/Limits.lean @@ -15,6 +15,8 @@ public import Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects -- shake: -- This import adds an instance which, despite failing to trigger, -- is necessary for some typeclass syntheses in this file to succeed. +meta import Lean.PostprocessTraces + /-! # (Co)Limits of Schemes @@ -33,6 +35,8 @@ We construct various limits and colimits in the category of schemes. -/ +open Lean.PostprocessTraces + @[expose] public section suppress_compilation @@ -232,9 +236,150 @@ noncomputable instance [Small.{u} σ] : CoproductsOfShapeDisjoint Scheme.{u} σ instance : HasFiniteCoproducts Scheme.{u} where out := inferInstance +/-! # Issue -/ + +set_option linter.style.longLine false in +#adaptation_note +/-- +instanceTypes-related fix: + +Was: +```lean set_option backward.isDefEq.respectTransparency.types false in instance : MonoCoprod Scheme.{u} := - .mk' fun X Y ↦ ⟨.mk coprod.inl coprod.inr, coprodIsCoprod X Y, inferInstanceAs <| Mono coprod.inl⟩ + .mk' fun X Y ↦ + ⟨.mk coprod.inl coprod.inr, coprodIsCoprod X Y, inferInstanceAs <| Mono coprod.inl⟩ +``` + +Why? +The inline inferInstanceAs leads to a two-step transitive unification: +`(BinaryCofan.mk ..).inl =?= coprod.inl (params obtained by unification from LHS) =?= + coprod.inl (from inl_of_binaryCoproductDisjoint's type)`. +The first comparison happens at a higher transparency than the second. Seems fragile. +The first unification has leeway regarding how the expression should look. +The second comparison happens at instance transparency. +-/ +instance : MonoCoprod Scheme.{u} := + .mk' fun X Y ↦ + ⟨.mk coprod.inl coprod.inr, coprodIsCoprod X Y, inferInstanceAs <| Mono coprod.inl (X := X)⟩ + +/-! ## Explanation -/ + +-- Without the `(X := X)` pin, `inferInstanceAs <| Mono coprod.inl` synthesizes via +-- `Mono.inl_of_binaryCoproductDisjoint`, which reduces to assigning an instance-typed mvar +-- `(?m : HasBinaryCoproduct ((pair X Y).obj {left}) Y) := (instHasColimit (pair X Y) : HasColimit +-- (pair X Y))`. +-- Under `"markOrSynth"` (as under `"mark"`) the direct `.instances` check fails — `(pair X Y).obj +-- {left}` does not reduce to `X` at instance transparency — so re-synthesis runs, succeeds, but +-- returns an instance for the *reduced* type; unifying it back against the original then fails, +-- and the assignment is rejected. So the problem form still fails to synthesize (the demo below +-- reproduces the failure); the real declaration above fixes it up front by pinning `(X := X)`. +-- Note: an alternative fix is to make `pair` implicit-reducible. In that case, this instance +-- would still fail to synthesize, but *a different* instance would succeed. + +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +set_option linter.style.longLine false in +/-- +error: failed to synthesize + Mono coprod.inl + +Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. +--- +trace: [Meta.synthInstance] ❌️ Mono coprod.inl + [Meta.synthInstance.apply] ❌️ apply @Mono.inl_of_binaryCoproductDisjoint to Mono coprod.inl + [Meta.synthInstance.tryResolve] ❌️ Mono coprod.inl ≟ Mono coprod.inl + [Meta.isDefEq] ❌️ [instances] Mono coprod.inl =?= Mono coprod.inl + [Meta.isDefEq] ❌️ [instances] coprod.inl =?= coprod.inl + [Meta.isDefEq] ❌️ [implicit] Scheme.IsLocallyDirected.instHasColimit (pair X Y) =?= ?m.49 + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.49 : HasBinaryCoproduct ((pair X Y).obj { as := WalkingPair.left }) + Y) := (Scheme.IsLocallyDirected.instHasColimit (pair X Y) : HasColimit (pair X Y)) + [Meta.isDefEq] ❌️ [instances] HasBinaryCoproduct ((pair X Y).obj { as := WalkingPair.left }) + Y =?= HasColimit (pair X Y) + [Meta.isDefEq] ❌️ [instances] HasColimit + (pair ((pair X Y).obj { as := WalkingPair.left }) Y) =?= HasColimit (pair X Y) + [Meta.isDefEq] ❌️ [instances] pair ((pair X Y).obj { as := WalkingPair.left }) Y =?= pair X Y + [Meta.isDefEq] ❌️ [instances] (pair X Y).obj { as := WalkingPair.left } =?= X + [Meta.isDefEq] ❌️ [instances] (pair X Y).1 { as := WalkingPair.left } =?= X + [Meta.isDefEq.onFailure] ❌️ (pair X Y).1 { as := WalkingPair.left } =?= X + [Meta.isDefEq.onFailure] ❌️ pair ((pair X Y).obj { as := WalkingPair.left }) Y =?= pair X Y + [Meta.isDefEq.onFailure] ❌️ HasColimit + (pair ((pair X Y).obj { as := WalkingPair.left }) Y) =?= HasColimit (pair X Y) + [Meta.synthInstance] ✅️ HasBinaryCoproduct ((pair X Y).obj { as := WalkingPair.left }) Y (truncated) + [Meta.isDefEq] ❌️ [implicit] Scheme.IsLocallyDirected.instHasColimit + (pair X + Y) =?= Scheme.IsLocallyDirected.instHasColimit + (pair ((pair X Y).obj { as := WalkingPair.left }) Y) + [Meta.isDefEq] ❌️ [implicit] HasColimit + (pair X Y) =?= HasColimit (pair ((pair X Y).obj { as := WalkingPair.left }) Y) + [Meta.isDefEq] ❌️ [implicit] pair X Y =?= pair ((pair X Y).obj { as := WalkingPair.left }) Y + [Meta.isDefEq] ❌️ [implicit] X =?= (pair X Y).obj { as := WalkingPair.left } + [Meta.isDefEq] ❌️ [implicit] X =?= (pair X Y).1 { as := WalkingPair.left } + [Meta.isDefEq.onFailure] ❌️ X =?= (pair X Y).1 { as := WalkingPair.left } + [Meta.isDefEq.onFailure] ❌️ pair X Y =?= pair ((pair X Y).obj { as := WalkingPair.left }) Y + [Meta.isDefEq.onFailure] ❌️ HasColimit + (pair X Y) =?= HasColimit (pair ((pair X Y).obj { as := WalkingPair.left }) Y) + [Meta.isDefEq] ❌️ [instances] colimit.ι (pair ((pair X Y).obj { as := WalkingPair.left }) Y) + { + as := + WalkingPair.left } =?= colimit.ι (pair ((pair X Y).obj { as := WalkingPair.left }) ?m.47) + { as := WalkingPair.left } + [Meta.isDefEq] ❌️ [implicit] Scheme.IsLocallyDirected.instHasColimit (pair X Y) =?= ?m.49 + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.49 : HasBinaryCoproduct + ((pair X Y).obj { as := WalkingPair.left }) + Y) := (Scheme.IsLocallyDirected.instHasColimit (pair X Y) : HasColimit (pair X Y)) + [Meta.isDefEq] ❌️ [instances] HasBinaryCoproduct ((pair X Y).obj { as := WalkingPair.left }) + Y =?= HasColimit (pair X Y) + [Meta.isDefEq] ❌️ [instances] HasColimit + (pair ((pair X Y).obj { as := WalkingPair.left }) Y) =?= HasColimit (pair X Y) + [Meta.isDefEq] ❌️ [instances] pair ((pair X Y).obj { as := WalkingPair.left }) Y =?= pair X Y + [Meta.isDefEq] ❌️ [instances] (pair X Y).obj { as := WalkingPair.left } =?= X + [Meta.isDefEq] ❌️ [instances] (pair X Y).1 { as := WalkingPair.left } =?= X + [Meta.isDefEq.onFailure] ❌️ (pair X Y).1 { as := WalkingPair.left } =?= X + [Meta.isDefEq.onFailure] ❌️ pair ((pair X Y).obj { as := WalkingPair.left }) Y =?= pair X Y + [Meta.isDefEq.onFailure] ❌️ HasColimit + (pair ((pair X Y).obj { as := WalkingPair.left }) Y) =?= HasColimit (pair X Y) + [Meta.synthInstance] ✅️ HasBinaryCoproduct ((pair X Y).obj { as := WalkingPair.left }) Y (truncated) + [Meta.isDefEq] ❌️ [implicit] Scheme.IsLocallyDirected.instHasColimit + (pair X + Y) =?= Scheme.IsLocallyDirected.instHasColimit + (pair ((pair X Y).obj { as := WalkingPair.left }) Y) + [Meta.isDefEq] ❌️ [implicit] HasColimit + (pair X Y) =?= HasColimit (pair ((pair X Y).obj { as := WalkingPair.left }) Y) + [Meta.isDefEq] ❌️ [implicit] pair X Y =?= pair ((pair X Y).obj { as := WalkingPair.left }) Y + [Meta.isDefEq] ❌️ [implicit] X =?= (pair X Y).obj { as := WalkingPair.left } + [Meta.isDefEq] ❌️ [implicit] X =?= (pair X Y).1 { as := WalkingPair.left } + [Meta.isDefEq.onFailure] ❌️ X =?= (pair X Y).1 { as := WalkingPair.left } + [Meta.isDefEq.onFailure] ❌️ pair X Y =?= pair ((pair X Y).obj { as := WalkingPair.left }) Y + [Meta.isDefEq.onFailure] ❌️ HasColimit + (pair X Y) =?= HasColimit (pair ((pair X Y).obj { as := WalkingPair.left }) Y) +-/ +#guard_msgs in +postprocess_traces + filterSubtrees (containsString "apply @CategoryTheory.Mono.inl_of_binaryCoproductDisjoint to") + >=> filterSubtrees (fun x => (ofClass `Meta.isDefEq.assign.checkTypes x) <&&> (failed x)) + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> (succeeded x)) +in +set_option trace.Meta.synthInstance true in +set_option trace.Meta.isDefEq true in +set_option trace.Meta.isDefEq.printTransparency true in +set_option trace.Meta.isDefEq.assign.checkTypes true in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option backward.isDefEq.respectTransparency.types false in +example : MonoCoprod Scheme.{u} := + .mk' fun X Y ↦ + ⟨.mk coprod.inl coprod.inr, coprodIsCoprod X Y, inferInstanceAs <| Mono coprod.inl⟩ + /-- The cover of `∐ X` by the `Xᵢ`. -/ @[simps!] diff --git a/mathlib4/Mathlib/AlgebraicGeometry/Modules/Tilde.lean b/mathlib4/Mathlib/AlgebraicGeometry/Modules/Tilde.lean index dee5b8e11..eb901d9da 100644 --- a/mathlib4/Mathlib/AlgebraicGeometry/Modules/Tilde.lean +++ b/mathlib4/Mathlib/AlgebraicGeometry/Modules/Tilde.lean @@ -12,6 +12,8 @@ public import Mathlib.Algebra.Module.LocalizedModule.Away public import Mathlib.AlgebraicGeometry.Modules.Sheaf public import Mathlib.Data.Fintype.Order +meta import Lean.PostprocessTraces + /-! # Construction of M^~ @@ -25,6 +27,10 @@ such that `M^~(U)` is the set of dependent functions that are locally fractions. -/ +set_option backward.isDefEq.instanceTypes "mark" + +open Lean.PostprocessTraces + @[expose] public noncomputable section universe u @@ -468,6 +474,10 @@ instance : (tilde M).IsQuasicoherent := instance : ((tilde.functor R).obj M).IsQuasicoherent := inferInstanceAs <| (tilde M).IsQuasicoherent +/-! # Issue -/ + +set_option backward.isDefEq.instanceTypes "markOrSynth" in +-- attribute [local instance_reducible] Scheme.Modules in set_option backward.isDefEq.respectTransparency false in lemma isIso_fromTildeΓ_of_presentation (M : (Spec R).Modules) (P : M.Presentation) : IsIso M.fromTildeΓ := by @@ -481,6 +491,85 @@ lemma isIso_fromTildeΓ_of_presentation (M : (Spec R).Modules) (P : M.Presentati exact ⟨cokernel g, ⟨PreservesCokernel.iso (tilde.functor R) g ≪≫ iso ≪≫ IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) P.isColimit⟩⟩ +set_option linter.style.longLine false +/-! ## Explanation + +The `iso` equivalence in the proof mixes the two spellings of the same category: its cokernels are +built by `tilde.functor R` (target `Scheme.Modules`) while `P.relations` lives in `SheafOfModules`. +Unifying them forces the instance-typed assignment +`(?inst : Category (Spec R).Modules) := (SheafOfModules.instCategory : Category (SheafOfModules …))`. +Under `"mark"` this check runs at `.instances`, where `Scheme.Modules` does not unfold, and it is +rejected — synthesizing `HasZeroMorphisms`/`Preadditive`/`Category` on `(Spec R).Modules` then fails. +Under `"markOrSynth"` the check runs at `.default`, unfolding `(Spec R).Modules` to +`SheafOfModules (Spec R).ringCatSheaf`, so the assignment is accepted and the proof goes through. +(The step recurs during the `rw`; the trace below shows one representative occurrence, keeping the +enclosing `synthInstance`/`apply` ancestry so the reader sees which instance search triggers it.) +-/ + +private meta def keepFirst : TracePostprocessor := fun roots => return roots.extract 0 1 + +private meta partial def maxDepth (depth : Nat) : TracePostprocessor := fun trees => + let rec truncateTree (t : TraceTree) (depth : Nat) : TraceTree := + match t with + | .leaf msg => TraceTree.leaf msg + | .node data msg children wrap => + match depth with + | 0 => .node data m!"{msg} (truncated)" #[] wrap + | depth' + 1 => .node data msg (children.map (truncateTree · depth')) wrap + return trees.map (truncateTree · depth) + +set_option linter.style.longLine false in +/-- +trace: [Meta.synthInstance] ✅️ HasZeroMorphisms (Spec (CommRingCat.of ↑R)).Modules + [Meta.synthInstance.apply] ✅️ apply @NonPreadditiveAbelian.toHasZeroMorphisms to HasZeroMorphisms + (Spec (CommRingCat.of ↑R)).Modules + [Meta.synthInstance.tryResolve] ✅️ HasZeroMorphisms + (Spec (CommRingCat.of ↑R)).Modules ≟ HasZeroMorphisms (Spec (CommRingCat.of ↑R)).Modules + [Meta.isDefEq] ✅️ [instances] HasZeroMorphisms (Spec (CommRingCat.of ↑R)).Modules =?= HasZeroMorphisms ?m.69 + [Meta.isDefEq] ✅️ [instances] SheafOfModules.instCategory =?= ?m.70 + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.70 : Category.{?u.41, u + 1} + (Spec + (CommRingCat.of + ↑R)).Modules) := (SheafOfModules.instCategory : Category.{u, u + 1} + (SheafOfModules (Spec R).ringCatSheaf)) + [Meta.isDefEq] ✅️ [default] Category.{?u.41, u + 1} + (Spec (CommRingCat.of ↑R)).Modules =?= Category.{u, u + 1} (SheafOfModules (Spec R).ringCatSheaf) + [Meta.isDefEq] ✅️ [default] (Spec (CommRingCat.of ↑R)).Modules =?= SheafOfModules (Spec R).ringCatSheaf + [Meta.isDefEq] ✅️ [default] SheafOfModules + (Spec (CommRingCat.of ↑R)).ringCatSheaf =?= SheafOfModules (Spec R).ringCatSheaf (truncated) +--- +warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended for development and not for final code. If you intend to submit this contribution to the Mathlib project, please remove 'set_option trace.Meta.synthInstance'. + +Note: This linter can be disabled with `set_option linter.style.setOption false` +-/ +#guard_msgs in +postprocess_traces + filterSubtrees (fun x => (ofClass `Meta.synthInstance.apply x) <&&> + (containsString "NonPreadditiveAbelian.toHasZeroMorphisms" x)) + >=> keepFirst + >=> filterSubtrees (fun x => (ofClass `Meta.isDefEq.assign.checkTypes x) <&&> + (containsString "SheafOfModules.instCategory" x) <&&> (containsString ".Modules)" x)) + >=> maxDepth 8 +in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option backward.isDefEq.respectTransparency false in +example (M : (Spec R).Modules) (P : M.Presentation) : + IsIso M.fromTildeΓ := by + set_option trace.Meta.synthInstance true in + set_option trace.Meta.isDefEq true in + set_option trace.Meta.isDefEq.printTransparency true in + set_option trace.Meta.isDefEq.assign.checkTypes true in + rw [isIso_fromTildeΓ_iff] + let g := (tilde.functor _).preimage <| (tildeFinsupp _).hom ≫ P.relations.π ≫ kernel.ι _ ≫ + (tildeFinsupp _).inv + let iso : cokernel ((tilde.functor R).map g) ≅ cokernel (P.relations.π ≫ kernel.ι _) := by + refine cokernel.mapIso _ _ (tildeFinsupp _) (tildeFinsupp _) ?_ + simp only [g, (tilde.functor R).map_preimage] + simp + exact ⟨cokernel g, ⟨PreservesCokernel.iso (tilde.functor R) g ≪≫ iso ≪≫ + IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) P.isColimit⟩⟩ + + section IsLocalizing variable (M : (Spec R).Modules) (f : R) {S : CommRingCat.{u}} (φ : R ⟶ S) diff --git a/mathlib4/Mathlib/AlgebraicGeometry/Morphisms/Flat.lean b/mathlib4/Mathlib/AlgebraicGeometry/Morphisms/Flat.lean index d1c1232c4..42d0eb9c4 100644 --- a/mathlib4/Mathlib/AlgebraicGeometry/Morphisms/Flat.lean +++ b/mathlib4/Mathlib/AlgebraicGeometry/Morphisms/Flat.lean @@ -11,6 +11,8 @@ public import Mathlib.AlgebraicGeometry.Properties public import Mathlib.AlgebraicGeometry.PullbackCarrier public import Mathlib.RingTheory.RingHom.FaithfullyFlat +meta import Lean.PostprocessTraces + /-! # Flat morphisms @@ -22,6 +24,10 @@ We show that this property is local, and are stable under compositions and base -/ +set_option backward.isDefEq.instanceTypes "mark" + +open Lean.PostprocessTraces + public section noncomputable section @@ -336,6 +342,11 @@ lemma mono_pushoutSection_of_iSup_eq {ι : Type*} [Finite ι] (VX : ι → X.Ope ext x j simp [ψY, H₂, -CommRingCat.hom_comp, ← CategoryTheory.comp_apply, pushoutSection, ψ] +/-! # Issue -/ + +set_option backward.isDefEq.instanceTypes "markOrSynth" in +-- set_option allowUnsafeReducibility true in +-- attribute [local instance_reducible] Pairwise.diagram Pairwise.diagramObj Functor.op set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma isIso_pushoutSection_of_iSup_eq @@ -437,6 +448,142 @@ lemma isIso_pushoutSection_of_iSup_eq · simp [αF, c, Under.liftCone, c', c₀] · simp [αF, c, c'] +/-! ## Explanation -/ + +/- +Why the real declaration above needs `"markOrSynth"`, reproduced by the demo below: +synthesizing `Mono (αF.app (op (pair i j)))` applies the hypothesis `hV'`; its resolution +assigns the resulting instance to a metavariable, re-checking the types with the +`(?m : Mono (pushoutSection …)) := (hV' i j : Mono (pushoutSection …))` assignment below. +The direct `.instances` check fails: with no metavariables left on the right, `tryHeuristic` +no longer compares by congruence but falls back to delta, unfolding `pushoutSection` on both +sides so its implicit arguments are compared at the stricter `.instances` transparency. +Under `"mark"` the assignment is then rejected and synthesis fails; under `"markOrSynth"` the +rejected instance is re-synthesized at its own type (`✅ Mono (pushoutSection …)`, returning +`hV' i j`) and the fresh instance unifies (`✅ hV' i j =?= hV' i j`), so the assignment is +accepted and the proof goes through. +-/ + +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +private meta def keepFirst : TracePostprocessor := fun roots => return roots.extract 0 1 + +set_option linter.style.longLine false in +/-- +trace: [Meta.synthInstance] ✅️ Mono (αF.app (op (Pairwise.pair i j))) + [Meta.isDefEq] ✅️ [instances] ?m.1066 =?= hV' i j + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.1066 : Mono + (pushoutSection H hUST ⋯ ⋯)) := (hV' i j : Mono (pushoutSection H hUST ⋯ ⋯)) + [Meta.isDefEq] ❌️ [instances] Mono (pushoutSection H hUST ⋯ ⋯) =?= Mono (pushoutSection H hUST ⋯ ⋯) (truncated) + [Meta.synthInstance] ✅️ Mono (pushoutSection H hUST ⋯ ⋯) (truncated) + [Meta.isDefEq] ✅️ [instances] hV' i j =?= hV' i j +--- +warning: declaration uses `sorry` +--- +warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended for development and not for final code. If you intend to submit this contribution to the Mathlib project, please remove 'set_option trace.Meta.synthInstance'. + +Note: This linter can be disabled with `set_option linter.style.setOption false` +-/ +#guard_msgs in +postprocess_traces + filterSubtrees (fun x => (ofClass `Meta.isDefEq.assign.checkTypes x) <&&> (containsString "hV' i j" x)) + >=> keepFirst + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> (succeeded x) <&&> + (containsString "pushoutSection" x)) + >=> elideBelow (fun x => (ofClass `Meta.isDefEq x) <&&> (failed x)) +in +set_option allowUnsafeReducibility true in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option backward.defeqAttrib.useBackward true in +set_option backward.isDefEq.respectTransparency false in +-- attribute [local instance_reducible] Pairwise.diagram Pairwise.diagramObj Functor.op in +example + {ι : Type u} [Finite ι] (VX : ι → X.Opens) (hVU : iSup VX = UX) + (hV : ∀ i, IsIso (pushoutSection H hUST (show VX i ≤ _ by aesop) rfl)) + (hV' : ∀ i j, Mono (pushoutSection H hUST + (show VX i ⊓ VX j ≤ _ from inf_le_left.trans (by clear hV; aesop)) rfl)) + (hT : (f.appLE US UT hUST).hom.Flat) : + IsIso (pushoutSection H hUST hUSX hUY) := by + classical + /- + We shall show that `Γ(T, Uₜ) ⊗[Γ(S, Uₛ)] Γ(X, U) ⟶ Γ(X ×ₛ T, pr₁ ⁻¹ U ∩ pr₂ ⁻¹ Uₜ)` is + injective using the following diagram + ``` + 0 → Γ(T, Uₜ) ⊗ Γ(X, U) ------→ Γ(T, Uₜ) ⊗ ∏ᵢ Γ(X, Vᵢ) ---→ Γ(T, Uₜ) ⊗ ∏ᵢⱼ Γ(X, Vᵢ ∩ Vⱼ) + | | | + ↓ ↓ ↓ + 0 → Γ(X ×ₛ T, U ∩ Uₜ) ------→ ∏ᵢ Γ(X ×ₛ T, Vᵢ ∩ Uₜ) ---→ ∏ᵢ Γ(X ×ₛ T, Vᵢ ∩ Vⱼ ∩ Uₜ) + ``` + The two rows are exact because of the sheaf axiom (and additionally the flatness assumption for + the top row). The vertical arrow in the middle is an isomorphism by assumption, and the one + one the right is monomorphic by assumption. Hence the left arrow is also an isomorphism. + + In the actual proof we use `Pairwise`-indexed diagrams instead of nested limits because it works + better with the existing API. + -/ + -- The diagram consisting of `Γ(X, Vᵢ) ⟶ Γ(X, Vᵢ ∩ Vⱼ)`. + let D := Pairwise.diagram VX + have h : iSup D.obj = UX := by + refine le_antisymm (iSup_le_iff.mpr ?_) ?_ + · subst hVU; rintro (i | ⟨i, j⟩); exacts [le_iSup VX _, inf_le_left.trans (le_iSup VX _)] + · subst hVU; exact iSup_le_iff.mpr fun i ↦ le_iSup D.obj (.single i) + let c₀ : Cocone D := (colimit.cocone _).extend + (eqToIso (Y := UX) (by simpa [CompleteLattice.colimit_eq_iSup])).hom + -- The diagram consisting of `Γ(T, Uₜ) ⊗ Γ(X, Vᵢ) ⟶ Γ(T, Uₜ) ⊗ Γ(X, Vᵢ ∩ Vⱼ)`. + let F := Under.lift _ ((Functor.const _).map (iX.appLE US UX hUSX) ≫ + ((X.presheaf.mapCone c₀.op).π)) ⋙ Under.pushout (f.appLE US UT hUST) ⋙ Under.forget _ + let G : X.Opens ⥤ Y.Opens := + { obj U := g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map h := homOfLE (by gcongr; exact h.le) } + -- The natural transformation between the diagrams at the top and bottom. + let αF : F ⟶ D.op ⋙ G.op ⋙ Y.presheaf := + { app i := (pushout.congrHom (by simp) rfl).hom ≫ + pushoutSection H hUST (by grw [← hUSX, ← h]; exact le_iSup D.obj i.unop) rfl } + -- `Γ(T, Uₜ) ⊗ Γ(X, U)` as a (limit) cone over the top diagram. + let c : Cone F := (Under.pushout (f.appLE US UT hUST) ⋙ Under.forget _).mapCone + (Under.liftCone (X.presheaf.mapCone c₀.op) _) + have := CommRingCat.Under.preservesFiniteLimits_of_flat _ hT + cases nonempty_fintype ι + let hc : IsLimit c := + haveI HX := ((TopCat.Presheaf.isSheaf_iff_isSheafPreservesLimitPairwiseIntersections + _).mp X.IsSheaf VX).preserves (c := c₀.op) + haveI HX := (HX (IsColimit.extendIso _ (colimit.isColimit _)).op).some + isLimitOfPreserves (Under.pushout _ ⋙ Under.forget _) (Under.isLimitLiftCone _ _ HX) + let c'₀ : Cocone (D ⋙ G) := (colimit.cocone _).extend + (eqToIso (Y := UY) (by + simp only [colimit.cocone_x, CompleteLattice.colimit_eq_iSup] + eta_expand + dsimp [G] + rw [← iSup_inf_eq, ← Scheme.Hom.preimage_iSup, h, hUY])).hom + -- `Γ(X ×ₛ T, U ∩ Uₜ)` as a (limit) cone over the bottom diagram. + let c' : Cone (D.op ⋙ G.op ⋙ Y.presheaf) := Y.presheaf.mapCone c'₀.op + let hc' : IsLimit c' := by + letI e : D ⋙ G ≅ Pairwise.diagram fun i ↦ g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT := + NatIso.ofComponents (fun | .single i => .refl _ | .pair i j => eqToIso (by + dsimp [D, G]; rw [Scheme.Hom.preimage_inf, inf_inf_distrib_right])) + haveI HX := ((TopCat.Presheaf.isSheaf_iff_isSheafPreservesLimitPairwiseIntersections _).mp + Y.IsSheaf (fun i ↦ g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT)).preserves + (c := ((Cocone.precompose e.inv).obj c'₀).op) + exact (IsLimit.postcomposeHomEquiv (Functor.isoWhiskerRight (NatIso.op e.symm) Y.presheaf) _) + ((HX ((IsColimit.precomposeInvEquiv e _).symm + (IsColimit.extendIso _ (colimit.isColimit _))).op).some.ofIsoLimit (Cone.ext (.refl _))) + have HαF₂ (i j : _) : Mono (αF.app (.op <| .pair i j)) := by + set_option trace.Meta.synthInstance true in + set_option trace.Meta.isDefEq true in + set_option trace.Meta.isDefEq.printTransparency true in + set_option trace.Meta.isDefEq.assign.checkTypes true in + infer_instance + sorry + lemma mono_pushoutSection_of_isCompact_of_flat_right [Flat f] (hUS : IsAffineOpen US) (hUT : IsAffineOpen UT) (hUX : IsCompact (X := X) UX) : Mono (pushoutSection H hUST hUSX hUY) := by diff --git a/mathlib4/Mathlib/AlgebraicGeometry/Spec.lean b/mathlib4/Mathlib/AlgebraicGeometry/Spec.lean index 6d84a46dc..da1e753d7 100644 --- a/mathlib4/Mathlib/AlgebraicGeometry/Spec.lean +++ b/mathlib4/Mathlib/AlgebraicGeometry/Spec.lean @@ -12,6 +12,8 @@ public import Mathlib.Topology.Sheaves.SheafCondition.Sites public import Mathlib.Topology.Sheaves.Functors public import Mathlib.Algebra.Module.LocalizedModule.Basic +meta import Lean.PostprocessTraces + /-! # $Spec$ as a functor to locally ringed spaces. @@ -34,6 +36,8 @@ The adjunction `Γ ⊣ Spec` is constructed in `Mathlib/AlgebraicGeometry/GammaS -/ +set_option backward.isDefEq.instanceTypes "mark" + @[expose] public section @@ -41,6 +45,8 @@ The adjunction `Γ ⊣ Spec` is constructed in `Mathlib/AlgebraicGeometry/GammaS noncomputable section +open Lean.PostprocessTraces + universe u v namespace AlgebraicGeometry @@ -237,6 +243,9 @@ theorem localRingHom_comp_stalkIso {R S : CommRingCat.{u}} (f : R ⟶ S) (p : Pr simp only [AlgEquiv.commutes, RingEquiv.symm_apply_eq, AlgEquiv.coe_ringEquiv] exact stalkMap_toStalk_apply f p x +/-! # Issue -/ + +set_option backward.isDefEq.instanceTypes "markOrSynth" in set_option backward.isDefEq.respectTransparency false in /-- The induced map of a ring homomorphism on the prime spectra, as a morphism of locally ringed spaces. @@ -252,6 +261,95 @@ def Spec.locallyRingedSpaceMap {R S : CommRingCat.{u}} (f : R ⟶ S) : have : IsLocalHom (stalkIso R (p.comap f.hom)).symm := isLocalHom_equiv _ exact ((ha.of_map (stalkIso S p)).of_map _).of_map (stalkIso R (p.comap f.hom)).symm +/-! ## Explanation -/ + +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +/- Synthesizing `IsLocalHom (Localization.localRingHom …)` unifies the goal with the conclusion of +`Localization.isLocalHom_localRingHom`, forcing the propositional instance-typed argument + `(?m : (PrimeSpectrum.comap f p).asIdeal.IsPrime) + := ((PrimeSpectrum.comap f p).isPrime : (Ideal.comap f p.asIdeal).IsPrime)`. +The two `IsPrime` types are not equal at `.instances` (neither `Ideal.comap` nor +`PrimeSpectrum.comap` +unfolds there), so the direct `checkTypes` fails (`❌`). Under `"mark"` that ends the assignment and +synthesis fails outright; under `"markOrSynth"` the fallback re-synthesizes the instance at the +mvar's type (`✅`, truncated below) and the assignment goes through — which is why the real +declaration above compiles. -/ +set_option linter.style.longLine false in +/-- +trace: [Meta.synthInstance] ✅️ IsLocalHom + (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f) ⋯) + [Meta.synthInstance.apply] ✅️ apply @Localization.isLocalHom_localRingHom to IsLocalHom + (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f) ⋯) + [Meta.synthInstance.tryResolve] ✅️ IsLocalHom + (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f) + ⋯) ≟ IsLocalHom + (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f) + ⋯) + [Meta.isDefEq] ✅️ [instances] IsLocalHom + (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f) + ⋯) =?= IsLocalHom (Localization.localRingHom ?m.108 ?m.110 ?m.112 ?m.113) + [Meta.isDefEq] ✅️ [instances] Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) + p.asIdeal (CommRingCat.Hom.hom f) ⋯ =?= Localization.localRingHom ?m.108 ?m.110 ?m.112 ?m.113 + [Meta.isDefEq] ✅️ [instances] (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).isPrime =?= ?m.109 + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.109 : (Ideal.comap (CommRingCat.Hom.hom f) + p.asIdeal).IsPrime) := ((PrimeSpectrum.comap (CommRingCat.Hom.hom f) + p).isPrime : (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal.IsPrime) + [Meta.isDefEq] ❌️ [instances] (Ideal.comap (CommRingCat.Hom.hom f) + p.asIdeal).IsPrime =?= (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal.IsPrime + [Meta.isDefEq] ❌️ [instances] Ideal.comap (CommRingCat.Hom.hom f) + p.asIdeal =?= (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal + [Meta.isDefEq] ❌️ [instances] Ideal.comap (CommRingCat.Hom.hom f) + p.asIdeal =?= (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).1 + [Meta.isDefEq.onFailure] ❌️ Ideal.comap (CommRingCat.Hom.hom f) + p.asIdeal =?= (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).1 + [Meta.isDefEq.onFailure] ❌️ (Ideal.comap (CommRingCat.Hom.hom f) + p.asIdeal).IsPrime =?= (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal.IsPrime + [Meta.synthInstance] ✅️ (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal).IsPrime (truncated) + [Meta.isDefEq] ✅️ [instances] (PrimeSpectrum.comap (CommRingCat.Hom.hom f) + p).isPrime =?= Ideal.IsPrime.comap (CommRingCat.Hom.hom f) (truncated) +--- +warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended for development and not for final code. If you intend to submit this contribution to the Mathlib project, please remove 'set_option trace.Meta.synthInstance'. + +Note: This linter can be disabled with `set_option linter.style.setOption false` +-/ +#guard_msgs in +postprocess_traces + filterSubtrees (fun x => (ofClass `Meta.synthInstance x) <&&> (containsString "IsLocalHom" x)) + >=> filterSubtrees (containsString "isLocalHom_localRingHom") + >=> filterSubtrees (fun x => (ofClass `Meta.isDefEq.assign.checkTypes x) <&&> + (containsString "Ideal.comap" x) <&&> (containsString "IsPrime" x)) + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> (succeeded x) <&&> + (containsString "IsPrime" x)) + >=> elideBelow (fun x => (ofClass `Meta.isDefEq x) <&&> (succeeded x) <&&> + (containsString "Ideal.IsPrime.comap" x)) +in +set_option trace.Meta.synthInstance true in +set_option trace.Meta.isDefEq true in +set_option trace.Meta.isDefEq.printTransparency true in +set_option trace.Meta.isDefEq.assign.checkTypes true in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option backward.isDefEq.respectTransparency false in +example {R S : CommRingCat.{u}} (f : R ⟶ S) : + Spec.locallyRingedSpaceObj S ⟶ Spec.locallyRingedSpaceObj R := + LocallyRingedSpace.Hom.mk (Spec.sheafedSpaceMap f).hom fun p => + IsLocalHom.mk fun a ha => by + rw [← localRingHom_comp_stalkIso] at ha + dsimp at ha + have : IsLocalHom (stalkIso S p) := isLocalHom_equiv _ + have : IsLocalHom (stalkIso R (p.comap f.hom)).symm := isLocalHom_equiv _ + exact ((ha.of_map (stalkIso S p)).of_map _).of_map (stalkIso R (p.comap f.hom)).symm + @[simp] theorem Spec.locallyRingedSpaceMap_id (R : CommRingCat.{u}) : Spec.locallyRingedSpaceMap (𝟙 R) = 𝟙 (Spec.locallyRingedSpaceObj R) := diff --git a/mathlib4/Mathlib/AlgebraicGeometry/StructureSheaf.lean b/mathlib4/Mathlib/AlgebraicGeometry/StructureSheaf.lean index 9cded7882..3f2d3a476 100644 --- a/mathlib4/Mathlib/AlgebraicGeometry/StructureSheaf.lean +++ b/mathlib4/Mathlib/AlgebraicGeometry/StructureSheaf.lean @@ -10,6 +10,7 @@ public import Mathlib.Algebra.Category.Ring.Limits public import Mathlib.RingTheory.Spectrum.Prime.Topology public import Mathlib.Tactic.DepRewrite public import Mathlib.Topology.Sheaves.LocalPredicate +meta import Lean.PostprocessTraces /-! # The structure sheaf on `PrimeSpectrum R`. @@ -47,6 +48,7 @@ boundaries. -/ +set_option linter.style.longFile 0 universe u @@ -230,6 +232,9 @@ def structurePresheafInCommRingCat : Presheaf CommRingCat (PrimeSpectrum.Top R) map_one' := rfl map_zero' := rfl } +set_option linter.style.setOption false in +set_option linter.style.maxHeartbeats false in +set_option synthInstance.maxHeartbeats 30000 in instance (U : (Opens (PrimeSpectrum.Top R))ᵒᵖ) : Module ((structureSheafInType R R).obj.obj U) ((structureSheafInType R M).obj.obj U) := inferInstanceAs (Module (sectionsSubalgebra R _) (sectionsSubalgebraSubmodule M _)) @@ -493,6 +498,11 @@ theorem exists_le_iSup_basicOpen_and_smul_eq_smul_and_eq_const simp [Submonoid.smul_def, pow_succ', mul_smul] · simp +set_option linter.style.longLine false + +/-! # Issue (Low Severity) -/ + +set_option backward.isDefEq.instanceTypes "none" in set_option backward.isDefEq.respectTransparency false in theorem toBasicOpenₗ_surjective (f : R) : Function.Surjective (toBasicOpenₗ R M f) := by intro s @@ -517,6 +527,231 @@ theorem toBasicOpenₗ_surjective (f : R) : Function.Surjective (toBasicOpenₗ simp_rw [one_smul, Finset.smul_sum, Submonoid.smul_def, smul_comm (b i), hab _ i, ← smul_assoc, ← Finset.sum_smul, hc] +/-! ## Explanation -/ + +open Lean.PostprocessTraces + +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +-- The dual of `filterSubtrees`: drop matching subtrees (used to remove `onFailure` retry duplicates). +private meta partial def dropSubtrees (p : TracePattern) : TracePostprocessor := + fun trees => trees.filterMapM go +where + go (t : TraceTree) : Lean.CoreM (Option TraceTree) := do + if ← p t then + return none + match t with + | .leaf msg => return some (.leaf msg) + | .node data msg children wrap => return some (.node data msg (← children.filterMapM go) wrap) + +-- Keeps the first subtree matching `p` in pre-order and drops every later match (the cached +-- re-attempts of the same assignment); non-matching structure is preserved. A matched subtree is +-- kept whole and not searched for further matches, mirroring `filterSubtrees`. The sibling branches +-- that used to lead to the dropped matches are pruned afterwards by a following `filterSubtrees`. +private meta partial def keepFirstMatch (p : TracePattern) : TracePostprocessor := + fun trees => Prod.fst <$> goArray true trees +where + goArray (keep : Bool) (trees : Array TraceTree) : Lean.CoreM (Array TraceTree × Bool) := do + let mut out := #[] + let mut keep := keep + for t in trees do + let (t?, keep') ← goTree keep t + keep := keep' + if let some t := t? then out := out.push t + return (out, keep) + goTree (keep : Bool) (t : TraceTree) : Lean.CoreM (Option TraceTree × Bool) := do + if ← p t then + return if keep then (some t, false) else (none, false) + match t with + | .leaf msg => return (some (.leaf msg), keep) + | .node data msg children wrap => + let (children, keep) ← goArray keep children + return (some (.node data msg children wrap), keep) + +/- The load-bearing step is `simpa … using iU`: rewriting the goal with `← SetLike.coe_subset_coe` +forces synthesis of `IsConcreteLE (Opens (PrimeSpectrum R)) …`, whose `SetLike` field is assigned the +candidate `Opens.instSetLike`. The `checkTypes` for that assignment compares the mvar type +`SetLike (Opens (PrimeSpectrum R)) ↑(PrimeSpectrum.Top R)` with the candidate type +`SetLike (Opens ↑(PrimeSpectrum.Top R)) ↑(PrimeSpectrum.Top R)`; they differ in the first `Opens` +argument and are not equal at `.instances` (`PrimeSpectrum.Top` does not unfold), so the direct check +fails (`❌`). The `markOrSynth` fallback re-synthesizes `SetLike (Opens (PrimeSpectrum R)) …`, which +recurses into a `TopologicalSpace (PrimeSpectrum R)` assignment: its direct check also fails, and +although synthesis does return `PrimeSpectrum.zariskiTopology` (`✅`, truncated), that instance is not +defeq at `.instances` to the candidate `(PrimeSpectrum.Top R).str`, so the assignment is rejected. With +no `SetLike`/`IsConcreteLE` instance found, `← SetLike.coe_subset_coe` never fires and `simpa` fails +with a type mismatch. Marking `PrimeSpectrum.Top` implicit-reducible fixes it (see `# Fix`). -/ +set_option linter.style.longLine false in +/-- +error: Type mismatch: After simplification, term + iU + has type + basicOpen f ≤ { carrier := (PrimeSpectrum.zeroLocus (Set.range b))ᶜ, is_open' := ⋯ } +but is expected to have type + PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f} +--- +trace: [Meta.synthInstance] ❌️ IsConcreteLE (Opens (PrimeSpectrum R)) ?B + [Meta.synthInstance.apply] ❌️ apply instIsConcreteLE to IsConcreteLE (Opens (PrimeSpectrum R)) ?m.114 + [Meta.synthInstance.tryResolve] ❌️ IsConcreteLE (Opens (PrimeSpectrum R)) ?m.114 ≟ IsConcreteLE ?m.117 ?m.118 + [Meta.isDefEq] ❌️ [instances] IsConcreteLE (Opens (PrimeSpectrum R)) ?m.114 =?= IsConcreteLE ?m.117 ?m.118 + [Meta.isDefEq] ❌️ [default] Opens.instPartialOrder.toLE =?= LE.ofSetLike (Opens (PrimeSpectrum R)) ?m.118 + [Meta.isDefEq] ❌️ [default] Opens.instPartialOrder.toLE =?= { le := fun H K ↦ ∀ ⦃x : ?m.118⦄, x ∈ H → x ∈ K } + [Meta.isDefEq] ❌️ [default] Opens.instPartialOrder.toPreorder.1 =?= { + le := fun H K ↦ ∀ ⦃x : ?m.118⦄, x ∈ H → x ∈ K } + [Meta.isDefEq] ❌️ [default] { + le := fun a a_1 ↦ + ∀ ⦃x : ↑(PrimeSpectrum.Top R)⦄, + x ∈ a → x ∈ a_1 } =?= { le := fun H K ↦ ∀ ⦃x : ?m.118⦄, x ∈ H → x ∈ K } + [Meta.isDefEq] ❌️ [default] fun a a_1 ↦ + ∀ ⦃x : ↑(PrimeSpectrum.Top R)⦄, x ∈ a → x ∈ a_1 =?= fun H K ↦ ∀ ⦃x : ?m.118⦄, x ∈ H → x ∈ K + [Meta.isDefEq] ❌️ [default] x ∈ a✝² =?= x ∈ a✝² + [Meta.isDefEq] ❌️ [default] SetLike.instMembership =?= SetLike.instMembership + [Meta.isDefEq] ❌️ [default] Opens.instSetLike =?= ?m.119 + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.119 : SetLike (Opens (PrimeSpectrum R)) + ↑(PrimeSpectrum.Top + R)) := (Opens.instSetLike : SetLike (Opens ↑(PrimeSpectrum.Top R)) + ↑(PrimeSpectrum.Top R)) + [Meta.isDefEq] ❌️ [instances] SetLike (Opens (PrimeSpectrum R)) + ↑(PrimeSpectrum.Top R) =?= SetLike (Opens ↑(PrimeSpectrum.Top R)) ↑(PrimeSpectrum.Top R) + [Meta.isDefEq] ❌️ [instances] Opens (PrimeSpectrum R) =?= Opens ↑(PrimeSpectrum.Top R) + [Meta.isDefEq] ❌️ [instances] PrimeSpectrum R =?= ↑(PrimeSpectrum.Top R) + [Meta.isDefEq] ❌️ [instances] PrimeSpectrum R =?= (PrimeSpectrum.Top R).1 + [Meta.synthInstance] ❌️ SetLike (Opens (PrimeSpectrum R)) ↑(PrimeSpectrum.Top R) + [Meta.synthInstance] ✅️ new goal SetLike (Opens (PrimeSpectrum R)) _tc.1 (truncated) + [Meta.synthInstance.apply] ❌️ apply @Opens.instSetLike to SetLike (Opens (PrimeSpectrum R)) + ?m.120 + [Meta.synthInstance.tryResolve] ❌️ SetLike (Opens (PrimeSpectrum R)) + ?m.120 ≟ SetLike (Opens ?m.122) ?m.122 + [Meta.isDefEq] ❌️ [instances] SetLike (Opens (PrimeSpectrum R)) + ?m.120 =?= SetLike (Opens ?m.122) ?m.122 + [Meta.isDefEq] ❌️ [instances] Opens (PrimeSpectrum R) =?= Opens ?m.122 + [Meta.isDefEq] ✅️ [instances] PrimeSpectrum R =?= ?m.122 + [Meta.isDefEq] PrimeSpectrum R [nonassignable] =?= ?m.122 [assignable] + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.122 : Type + ?u.54) := (PrimeSpectrum R : Type u) + [Meta.isDefEq] ✅️ [default] Type ?u.54 =?= Type u + [Meta.isDefEq] ❌️ [instances] (PrimeSpectrum.Top R).str =?= ?m.123 + [Meta.isDefEq] (PrimeSpectrum.Top R).str [nonassignable] =?= ?m.123 [assignable] + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.123 : TopologicalSpace + (PrimeSpectrum + R)) := ((PrimeSpectrum.Top + R).str : TopologicalSpace ↑(PrimeSpectrum.Top R)) + [Meta.isDefEq] ❌️ [instances] TopologicalSpace + (PrimeSpectrum R) =?= TopologicalSpace ↑(PrimeSpectrum.Top R) + [Meta.isDefEq] ❌️ [instances] PrimeSpectrum R =?= ↑(PrimeSpectrum.Top R) + [Meta.isDefEq] ❌️ [instances] PrimeSpectrum R =?= (PrimeSpectrum.Top R).1 + [Meta.synthInstance] ✅️ TopologicalSpace (PrimeSpectrum R) (truncated) + [Meta.isDefEq] ❌️ [instances] (PrimeSpectrum.Top + R).str =?= PrimeSpectrum.zariskiTopology + [Meta.isDefEq] ❌️ [instances] (PrimeSpectrum.Top + R).str =?= ofClosed (Set.range PrimeSpectrum.zeroLocus) ⋯ ⋯ ⋯ + [Meta.isDefEq] ❌️ [instances] (PrimeSpectrum.Top + R).str =?= { + IsOpen := fun X ↦ Xᶜ ∈ Set.range PrimeSpectrum.zeroLocus, + isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ } + [Meta.isDefEq] ❌️ [instances] (PrimeSpectrum.Top + R).2 =?= { + IsOpen := fun X ↦ Xᶜ ∈ Set.range PrimeSpectrum.zeroLocus, + isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ } + [Meta.isDefEq] ❌️ [instances] TopologicalSpace + (PrimeSpectrum.Top R).1 =?= TopologicalSpace (PrimeSpectrum R) + [Meta.isDefEq] ❌️ [instances] (PrimeSpectrum.Top + R).1 =?= PrimeSpectrum R + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.123 : TopologicalSpace + (PrimeSpectrum + R)) := ((PrimeSpectrum.Top + R).2 : TopologicalSpace (PrimeSpectrum.Top R).1) + [Meta.isDefEq] ❌️ [instances] TopologicalSpace + (PrimeSpectrum R) =?= TopologicalSpace (PrimeSpectrum.Top R).1 + [Meta.synthInstance] ✅️ TopologicalSpace (PrimeSpectrum R) (truncated) + [Meta.isDefEq] ❌️ [instances] (PrimeSpectrum.Top + R).2 =?= PrimeSpectrum.zariskiTopology + [Meta.isDefEq] ❌️ [instances] (PrimeSpectrum.Top + R).2 =?= ofClosed (Set.range PrimeSpectrum.zeroLocus) ⋯ ⋯ ⋯ + [Meta.isDefEq] ❌️ [instances] (PrimeSpectrum.Top + R).2 =?= { IsOpen := fun X ↦ Xᶜ ∈ Set.range PrimeSpectrum.zeroLocus, + isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ } + [Meta.isDefEq] ❌️ [instances] TopologicalSpace + (PrimeSpectrum.Top R).1 =?= TopologicalSpace (PrimeSpectrum R) + [Meta.isDefEq] ❌️ [instances] (PrimeSpectrum.Top + R).1 =?= PrimeSpectrum R + [Meta.synthInstance] result +-/ +#guard_msgs in +postprocess_traces + keepFirstMatch (fun x => do (ofClass `Meta.isDefEq.assign.checkTypes x) <&&> + (containsString "Opens.instSetLike" x)) + >=> filterSubtrees (fun x => do (ofClass `Meta.isDefEq.assign.checkTypes x) <&&> + (containsString "Opens.instSetLike" x)) + >=> dropSubtrees (fun x => ofClass `Meta.isDefEq.onFailure x) + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> succeeded x) +in +set_option trace.Meta.synthInstance true in +set_option trace.Meta.isDefEq true in +set_option trace.Meta.isDefEq.printTransparency true in +set_option trace.Meta.isDefEq.assign.checkTypes true in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option backward.isDefEq.respectTransparency false in +example (f : R) : Function.Surjective (toBasicOpenₗ R M f) := by + intro s + obtain ⟨ι, _, a, b, ibU, iU, hab, H⟩ := exists_le_iSup_basicOpen_and_smul_eq_smul_and_eq_const _ + (PrimeSpectrum.isCompact_basicOpen _) s + obtain ⟨n, hn⟩ : f ∈ (Ideal.span (Set.range b)).radical := by + have : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f} := by + simpa [← SetLike.coe_subset_coe, ← Set.compl_iInter, + ← PrimeSpectrum.zeroLocus_iUnion, PrimeSpectrum.Top] using iU + rw [← PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.zeroLocus_span, + PrimeSpectrum.mem_vanishingIdeal] + exact fun x hx ↦ by simpa using this hx + replace hn := Ideal.mul_mem_right f _ hn + rw [← pow_succ, Ideal.span, Finsupp.mem_span_range_iff_exists_finsupp] at hn + obtain ⟨c, hc⟩ := hn + rw [Finsupp.sum_fintype _ _ (by simp)] at hc + refine ⟨LocalizedModule.mk (∑ i, c i • a i) ⟨f ^ (n + 1), _, rfl⟩, ?_⟩ + refine (structureSheafInType R M).eq_of_locally_eq' (fun i ↦ basicOpen (b i)) _ + (fun i ↦ (ibU _).hom) iU _ _ fun i ↦ (Subtype.ext (funext fun x ↦ ?_)).trans (H _).symm + rw [toBasicOpenₗ_mk] + refine LocalizedModule.mk_eq.mpr ⟨1, ?_⟩ + simp_rw [one_smul, Finset.smul_sum, Submonoid.smul_def, smul_comm (b i), hab _ i, ← smul_assoc, + ← Finset.sum_smul, hc] + +/-! # Fix -/ + +attribute [local implicit_reducible] PrimeSpectrum.Top in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +example (f : R) : Function.Surjective (toBasicOpenₗ R M f) := by + intro s + obtain ⟨ι, _, a, b, ibU, iU, hab, H⟩ := exists_le_iSup_basicOpen_and_smul_eq_smul_and_eq_const _ + (PrimeSpectrum.isCompact_basicOpen _) s + obtain ⟨n, hn⟩ : f ∈ (Ideal.span (Set.range b)).radical := by + have : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f} := by + simpa [← SetLike.coe_subset_coe, ← Set.compl_iInter, + ← PrimeSpectrum.zeroLocus_iUnion, PrimeSpectrum.Top] using iU + rw [← PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.zeroLocus_span, + PrimeSpectrum.mem_vanishingIdeal] + exact fun x hx ↦ by simpa using this hx + replace hn := Ideal.mul_mem_right f _ hn + rw [← pow_succ, Ideal.span, Finsupp.mem_span_range_iff_exists_finsupp] at hn + obtain ⟨c, hc⟩ := hn + rw [Finsupp.sum_fintype _ _ (by simp)] at hc + refine ⟨LocalizedModule.mk (∑ i, c i • a i) ⟨f ^ (n + 1), _, rfl⟩, ?_⟩ + refine (structureSheafInType R M).eq_of_locally_eq' (fun i ↦ basicOpen (b i)) _ + (fun i ↦ (ibU _).hom) iU _ _ fun i ↦ (Subtype.ext (funext fun x ↦ ?_)).trans (H _).symm + rw [toBasicOpenₗ_mk] + refine LocalizedModule.mk_eq.mpr ⟨1, ?_⟩ + simp_rw [one_smul, Finset.smul_sum, Submonoid.smul_def, smul_comm (b i), hab _ i, ← smul_assoc, + ← Finset.sum_smul, hc] + + set_option backward.isDefEq.respectTransparency.types false in public instance (f : R) : IsLocalizedModule.Away f (toOpenₗ R M (basicOpen f)) := by convert! @@ -794,6 +1029,8 @@ instance (x : PrimeSpectrum.Top R) : rw! [PrimeSpectrum.basicOpen_one] rfl + +set_option backward.isDefEq.instanceTypes "markOrSynth" in set_option backward.isDefEq.respectTransparency false in variable (R M) in /-- The canonical ring homomorphism interpreting an element of `R` as an element of diff --git a/mathlib4/Mathlib/Analysis/Real/Pi/Chudnovsky.lean b/mathlib4/Mathlib/Analysis/Real/Pi/Chudnovsky.lean index a1ff2d4c4..8aa136c18 100644 --- a/mathlib4/Mathlib/Analysis/Real/Pi/Chudnovsky.lean +++ b/mathlib4/Mathlib/Analysis/Real/Pi/Chudnovsky.lean @@ -5,7 +5,7 @@ Authors: Kim Morrison -/ module -meta import Batteries.Data.Rat.Float -- shake: keep (for `#eval` sanity check) +meta import Batteries.Data.Float.Rat -- shake: keep (for `#eval` sanity check) public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan public import Mathlib.MeasureTheory.Integral.Bochner.Basic public import Mathlib.Tactic.Positivity diff --git a/mathlib4/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean b/mathlib4/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean index fa4de714f..c1f98aae3 100644 --- a/mathlib4/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean +++ b/mathlib4/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean @@ -203,6 +203,9 @@ lemma top_mem_range (A₀ : Subobject X) {J : Type w} [LinearOrder J] [OrderBot top_mem_range_transfiniteIterate (largerSubobject hG) A₀ (lt_largerSubobject hG) (by simp) (fun h ↦ by simpa [hasCardinalLT_iff_cardinal_mk_lt] using hJ.of_injective _ h) +-- set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option linter.style.maxHeartbeats false in +set_option synthInstance.maxHeartbeats 30000 in lemma exists_ordinal (A₀ : Subobject X) : ∃ (o : Ordinal.{w}) (j : o.ToType), transfiniteIterate (largerSubobject hG) j A₀ = ⊤ := by let κ := Order.succ (Cardinal.mk (Shrink.{w} (Subobject X))) diff --git a/mathlib4/Mathlib/CategoryTheory/Abelian/Subobject.lean b/mathlib4/Mathlib/CategoryTheory/Abelian/Subobject.lean index 08831cebc..af5f61d68 100644 --- a/mathlib4/Mathlib/CategoryTheory/Abelian/Subobject.lean +++ b/mathlib4/Mathlib/CategoryTheory/Abelian/Subobject.lean @@ -8,11 +8,17 @@ module public import Mathlib.CategoryTheory.Subobject.Limits public import Mathlib.CategoryTheory.Abelian.Basic +meta import Lean.PostprocessTraces + /-! # Equivalence between subobjects and quotients in an abelian category -/ +set_option backward.isDefEq.instanceTypes "mark" + +open Lean.PostprocessTraces + @[expose] public section @@ -26,7 +32,22 @@ namespace CategoryTheory.Abelian variable {C : Type u} [Category.{v} C] +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +/-! # Issue (Low Severity) -/ + set_option backward.isDefEq.respectTransparency.types false in +set_option backward.isDefEq.instanceTypes "none" in set_option backward.defeqAttrib.useBackward true in /-- In an abelian category, the subobjects and quotient objects of an object `X` are order-isomorphic via taking kernels and cokernels. @@ -63,6 +84,192 @@ def subobjectIsoSubobjectOp [Abelian C] (X : C) : Subobject X ≃o (Subobject (o · simp only [← cancel_mono f, Category.assoc, monoLift_comp, image.fac, Category.id_comp] · simp only [monoLift_comp] +/-! +## Explanation + +Important observation: It even fails with "mapOrSynth". + +The mvar assignment happens at instance transparency: +It happens in `isDefEqArgsFirstPass`, which doesn't do an implicit bump. + +(Additionally: it's a propositional instance, and we don't bump when applying proof irrel: +``` +private def withProofIrrelTransparency (k : MetaM α) : MetaM α := do + if backward.isDefEq.respectTransparency.get (← getOptions) then + k + else + withInferTypeConfig k +``` + +See below for what the fix needs. +) +-/ +set_option linter.style.longLine false in +/-- +error: failed to synthesize instance of type class + Mono (kernel.ι (cokernel.π f)) +--- +error: No goals to be solved +--- +trace: [Meta.synthInstance] ❌️ Mono (kernel.ι (cokernel.π f)) + [Meta.synthInstance.apply] ❌️ apply @equalizer.ι_mono to Mono (kernel.ι (cokernel.π f)) + [Meta.synthInstance.tryResolve] ❌️ Mono (kernel.ι (cokernel.π f)) ≟ Mono (equalizer.ι ?m.244 ?m.245) + [Meta.isDefEq] ❌️ [instances] Mono (kernel.ι (cokernel.π f)) =?= Mono (equalizer.ι ?m.244 ?m.245) + [Meta.isDefEq] ❌️ [instances] kernel.ι (cokernel.π f) =?= equalizer.ι ?m.244 ?m.245 + [Meta.isDefEq] ❌️ [instances] equalizer.ι (cokernel.π f) 0 =?= equalizer.ι ?m.244 ?m.245 + [Meta.isDefEq] ❌️ [instances] kernelOrderHom._proof_1 X (op (cokernel f)) (cokernel.π f).op =?= ?m.246 + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.246 : HasEqualizer (cokernel.π f) + 0) := (kernelOrderHom._proof_1 X (op (cokernel f)) + (cokernel.π f).op : HasKernel (cokernel.π f).op.unop) + [Meta.isDefEq] ❌️ [instances] HasEqualizer (cokernel.π f) 0 =?= HasKernel (cokernel.π f).op.unop + [Meta.isDefEq] ❌️ [instances] HasLimit + (parallelPair (cokernel.π f) 0) =?= HasLimit (parallelPair (cokernel.π f).op.unop 0) + [Meta.isDefEq] ❌️ [instances] parallelPair (cokernel.π f) + 0 =?= parallelPair (cokernel.π f).op.unop 0 + [Meta.isDefEq] ❌️ [instances] cokernel.π f =?= (cokernel.π f).op.unop + [Meta.isDefEq] ❌️ [instances] coequalizer.π f 0 =?= (cokernel.π f).op.unop + [Meta.isDefEq] ❌️ [instances] colimit.ι (parallelPair f 0) + WalkingParallelPair.one =?= (cokernel.π f).op.unop + [Meta.isDefEq] ❌️ [instances] @colimit.ι =?= @Quiver.Hom.unop + [Meta.isDefEq.onFailure] ❌️ colimit.ι (parallelPair f 0) + WalkingParallelPair.one =?= (cokernel.π f).op.unop + [Meta.isDefEq.onFailure] ❌️ parallelPair (cokernel.π f) + 0 =?= parallelPair (cokernel.π f).op.unop 0 + [Meta.isDefEq.onFailure] ❌️ HasLimit + (parallelPair (cokernel.π f) 0) =?= HasLimit (parallelPair (cokernel.π f).op.unop 0) + [Meta.synthInstance] ✅️ HasEqualizer (cokernel.π f) 0 (truncated) + [Meta.isDefEq] ❌️ [instances] kernelOrderHom._proof_1 X (op (cokernel f)) + (cokernel.π f).op =?= HasKernels.has_limit (cokernel.π f) + [Meta.isDefEq] ❌️ [instances] HasKernel (cokernel.π f).op.unop =?= HasKernel (cokernel.π f) + [Meta.isDefEq] ❌️ [instances] HasLimit + (parallelPair (cokernel.π f).op.unop 0) =?= HasLimit (parallelPair (cokernel.π f) 0) + [Meta.isDefEq] ❌️ [instances] parallelPair (cokernel.π f).op.unop + 0 =?= parallelPair (cokernel.π f) 0 + [Meta.isDefEq] ❌️ [instances] (cokernel.π f).op.unop =?= cokernel.π f + [Meta.isDefEq] ❌️ [instances] (cokernel.π f).op.unop =?= coequalizer.π f 0 + [Meta.isDefEq] ❌️ [instances] (cokernel.π + f).op.unop =?= colimit.ι (parallelPair f 0) WalkingParallelPair.one + [Meta.isDefEq] ❌️ [instances] @Quiver.Hom.unop =?= @colimit.ι + [Meta.isDefEq.onFailure] ❌️ (cokernel.π + f).op.unop =?= colimit.ι (parallelPair f 0) WalkingParallelPair.one + [Meta.isDefEq.onFailure] ❌️ parallelPair (cokernel.π f).op.unop + 0 =?= parallelPair (cokernel.π f) 0 + [Meta.isDefEq.onFailure] ❌️ HasLimit + (parallelPair (cokernel.π f).op.unop 0) =?= HasLimit (parallelPair (cokernel.π f) 0) + [Meta.isDefEq] ❌️ [instances] limit.π (parallelPair (cokernel.π f) 0) + WalkingParallelPair.zero =?= limit.π (parallelPair ?m.244 ?m.245) WalkingParallelPair.zero + [Meta.isDefEq] ❌️ [instances] kernelOrderHom._proof_1 X (op (cokernel f)) (cokernel.π f).op =?= ?m.246 + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.246 : HasEqualizer (cokernel.π f) + 0) := (kernelOrderHom._proof_1 X (op (cokernel f)) + (cokernel.π f).op : HasKernel (cokernel.π f).op.unop) + [Meta.isDefEq] ❌️ [instances] HasEqualizer (cokernel.π f) 0 =?= HasKernel (cokernel.π f).op.unop + [Meta.isDefEq] ❌️ [instances] HasLimit + (parallelPair (cokernel.π f) 0) =?= HasLimit (parallelPair (cokernel.π f).op.unop 0) + [Meta.synthInstance] ✅️ HasEqualizer (cokernel.π f) 0 (truncated) + [Meta.isDefEq] ❌️ [instances] kernelOrderHom._proof_1 X (op (cokernel f)) + (cokernel.π f).op =?= HasKernels.has_limit (cokernel.π f) + [Meta.isDefEq] ❌️ [instances] HasKernel (cokernel.π f).op.unop =?= HasKernel (cokernel.π f) + [Meta.isDefEq] ❌️ [instances] HasLimit + (parallelPair (cokernel.π f).op.unop 0) =?= HasLimit (parallelPair (cokernel.π f) 0) + [Meta.isDefEq] ❌️ [instances] parallelPair (cokernel.π f).op.unop + 0 =?= parallelPair (cokernel.π f) 0 + [Meta.isDefEq] ❌️ [instances] (cokernel.π f).op.unop =?= cokernel.π f + [Meta.isDefEq] ❌️ [instances] (cokernel.π f).op.unop =?= coequalizer.π f 0 + [Meta.isDefEq] ❌️ [instances] (cokernel.π + f).op.unop =?= colimit.ι (parallelPair f 0) WalkingParallelPair.one + [Meta.isDefEq] ❌️ [instances] @Quiver.Hom.unop =?= @colimit.ι + [Meta.isDefEq.onFailure] ❌️ (cokernel.π + f).op.unop =?= colimit.ι (parallelPair f 0) WalkingParallelPair.one + [Meta.isDefEq.onFailure] ❌️ parallelPair (cokernel.π f).op.unop + 0 =?= parallelPair (cokernel.π f) 0 + [Meta.isDefEq.onFailure] ❌️ HasLimit + (parallelPair (cokernel.π f).op.unop 0) =?= HasLimit (parallelPair (cokernel.π f) 0) +-/ +#guard_msgs in +postprocess_traces + hoist (fun x => do (ofClass `Meta.synthInstance x) <&&> + (containsString "Mono (CategoryTheory.Limits.kernel.ι" x)) + >=> filterSubtrees (fun x => do (ofClass `Meta.isDefEq.assign.checkTypes x) <&&> + (containsString "kernelOrderHom" x)) + >=> filterSubtrees (containsString "equalizer.ι_mono") + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> (containsString "HasEqualizer" x)) +in +set_option trace.Meta.synthInstance true in +set_option trace.Meta.isDefEq true in +set_option trace.Meta.isDefEq.assign.checkTypes true in +set_option backward.isDefEq.respectTransparency.types false in +set_option backward.defeqAttrib.useBackward true in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +-- pin the pre-`firstPassBump` behavior: this block documents the old failure +set_option backward.isDefEq.firstPassBump false in +set_option trace.Meta.isDefEq.printTransparency true in +example [Abelian C] (X : C) : Subobject X ≃o (Subobject (op X))ᵒᵈ := by + refine OrderIso.ofHomInv (cokernelOrderHom X) (kernelOrderHom X) ?_ ?_ + · change (cokernelOrderHom X).comp (kernelOrderHom X) = _ + refine OrderHom.ext _ _ (funext (Subobject.ind _ ?_)) + intro A f hf + dsimp only [OrderHom.comp_coe, Function.comp_apply, kernelOrderHom_coe, Subobject.lift_mk, + cokernelOrderHom_coe, OrderHom.id_coe, id] + refine Subobject.mk_eq_mk_of_comm _ _ + ⟨?_, ?_, Quiver.Hom.unop_inj ?_, Quiver.Hom.unop_inj ?_⟩ ?_ + · exact (Abelian.epiDesc f.unop _ (cokernel.condition (kernel.ι f.unop))).op + · exact (cokernel.desc _ _ (kernel.condition f.unop)).op + · rw [← cancel_epi (cokernel.π (kernel.ι f.unop))] + simp only [unop_comp, Quiver.Hom.unop_op, unop_id_op, cokernel.π_desc_assoc, + comp_epiDesc, Category.comp_id] + · simp only [← cancel_epi f.unop, unop_comp, Quiver.Hom.unop_op, unop_id, comp_epiDesc_assoc, + cokernel.π_desc, Category.comp_id] + · exact Quiver.Hom.unop_inj (by simp only [unop_comp, Quiver.Hom.unop_op, comp_epiDesc]) + · change (kernelOrderHom X).comp (cokernelOrderHom X) = _ + refine OrderHom.ext _ _ (funext (Subobject.ind _ ?_)) + intro A f hf + dsimp only [OrderHom.comp_coe, Function.comp_apply, cokernelOrderHom_coe, Subobject.lift_mk, + kernelOrderHom_coe, OrderHom.id_coe, id, unop_op, Quiver.Hom.unop_op] + -- have : HasKernel (cokernel.π f).op.unop := inferInstance + -- have : HasEqualizer (cokernel.π f) 0 := inferInstance + refine Subobject.mk_eq_mk_of_comm _ _ ⟨?_, ?_, ?_, ?_⟩ ?_ + · exact Abelian.monoLift f _ (kernel.condition (cokernel.π f)) + · exact kernel.lift _ _ (cokernel.condition f) + · simp only [← cancel_mono (kernel.ι (cokernel.π f)), Category.assoc, image.fac, monoLift_comp, + Category.id_comp] + · simp only [← cancel_mono f, Category.assoc, monoLift_comp, image.fac, Category.id_comp] + · simp only [monoLift_comp] + +/- Fix: Needs `backward.isDefEq.firstPassBump` and `Quiver.Hom.op/unop` implicit-reducible -/ +attribute [local implicit_reducible] Quiver.Hom.op Quiver.Hom.unop in +set_option backward.isDefEq.respectTransparency.types false in +set_option backward.defeqAttrib.useBackward true in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +example [Abelian C] (X : C) : Subobject X ≃o (Subobject (op X))ᵒᵈ := by + refine OrderIso.ofHomInv (cokernelOrderHom X) (kernelOrderHom X) ?_ ?_ + · change (cokernelOrderHom X).comp (kernelOrderHom X) = _ + refine OrderHom.ext _ _ (funext (Subobject.ind _ ?_)) + intro A f hf + dsimp only [OrderHom.comp_coe, Function.comp_apply, kernelOrderHom_coe, Subobject.lift_mk, + cokernelOrderHom_coe, OrderHom.id_coe, id] + refine Subobject.mk_eq_mk_of_comm _ _ + ⟨?_, ?_, Quiver.Hom.unop_inj ?_, Quiver.Hom.unop_inj ?_⟩ ?_ + · exact (Abelian.epiDesc f.unop _ (cokernel.condition (kernel.ι f.unop))).op + · exact (cokernel.desc _ _ (kernel.condition f.unop)).op + · rw [← cancel_epi (cokernel.π (kernel.ι f.unop))] + simp only [unop_comp, Quiver.Hom.unop_op, unop_id_op, cokernel.π_desc_assoc, + comp_epiDesc, Category.comp_id] + · simp only [← cancel_epi f.unop, unop_comp, Quiver.Hom.unop_op, unop_id, comp_epiDesc_assoc, + cokernel.π_desc, Category.comp_id] + · exact Quiver.Hom.unop_inj (by simp only [unop_comp, Quiver.Hom.unop_op, comp_epiDesc]) + · change (kernelOrderHom X).comp (cokernelOrderHom X) = _ + refine OrderHom.ext _ _ (funext (Subobject.ind _ ?_)) + intro A f hf + dsimp only [OrderHom.comp_coe, Function.comp_apply, cokernelOrderHom_coe, Subobject.lift_mk, + kernelOrderHom_coe, OrderHom.id_coe, id, unop_op, Quiver.Hom.unop_op] + refine Subobject.mk_eq_mk_of_comm _ _ ⟨?_, ?_, ?_, ?_⟩ ?_ + · exact Abelian.monoLift f _ (kernel.condition (cokernel.π f)) + · exact kernel.lift _ _ (cokernel.condition f) + · simp only [← cancel_mono (kernel.ι (cokernel.π f)), Category.assoc, image.fac, monoLift_comp, + Category.id_comp] + · simp only [← cancel_mono f, Category.assoc, monoLift_comp, image.fac, Category.id_comp] + · simp only [monoLift_comp] + /-- A well-powered abelian category is also well-copowered. -/ instance wellPowered_opposite [Abelian C] [LocallySmall.{w} C] [WellPowered.{w} C] : WellPowered.{w} Cᵒᵖ where diff --git a/mathlib4/Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean b/mathlib4/Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean index b4d3226a7..94dc7fc49 100644 --- a/mathlib4/Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean +++ b/mathlib4/Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean @@ -12,6 +12,8 @@ public import Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit public import Mathlib.CategoryTheory.Limits.Preserves.Grothendieck public import Mathlib.CategoryTheory.Limits.Final +meta import Lean.PostprocessTraces + /-! # Inferring Filteredness from Filteredness of Costructured Arrow Categories @@ -21,6 +23,10 @@ public import Mathlib.CategoryTheory.Limits.Final -/ +set_option backward.isDefEq.instanceTypes "mark" + +open Lean.PostprocessTraces + public section universe v₁ v₂ v₃ u₁ u₂ u₃ @@ -34,6 +40,106 @@ section Small variable {A : Type u₁} [SmallCategory A] {B : Type u₁} [SmallCategory B] variable {T : Type u₁} [SmallCategory T] +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +/-! # Issue -/ + +-- `simp only [Cat.of_α]` rewrites the shape carrier of `colim` to `CostructuredArrow L (R.obj b)` +-- but leaves that `colim`'s `Category` instance typed at the old spelling +-- `↑(Cat.of (CostructuredArrow …))`. Synthesizing the lemma's `HasColimitsOfShape` argument (via +-- `Types.hasColimitsOfShape`) must reproduce this carrier-vs-instance mismatch through an +-- instance-typed mvar, which denies the assignment (trace below): the direct `.instances` check +-- can't cross the `CostructuredArrow =?= ↑(Cat.of …)` boundary, and under `markOrSynth` the +-- re-synthesis fallback finds `instCategoryCostructuredArrow_1`, which is not defeq to the unified +-- instance either. +set_option linter.style.longLine false in +/-- +error: failed to synthesize instance of type class + HasColimitsOfShape (CostructuredArrow L (R.obj b)) (Type u₁) +--- +trace: [Meta.synthInstance] ❌️ HasColimitsOfShape (CostructuredArrow L (R.obj b)) (Type u₁) + [Meta.synthInstance.apply] ❌️ apply @Types.hasColimitsOfShape to HasColimitsOfShape (CostructuredArrow L (R.obj b)) + (Type u₁) + [Meta.synthInstance.tryResolve] ❌️ HasColimitsOfShape (CostructuredArrow L (R.obj b)) + (Type u₁) ≟ HasColimitsOfShape ?m.79 (Type ?u.120) + [Meta.isDefEq] ❌️ [instances] HasColimitsOfShape (CostructuredArrow L (R.obj b)) + (Type u₁) =?= HasColimitsOfShape ?m.79 (Type ?u.120) + [Meta.isDefEq] ❌️ [instances] (Cat.of (CostructuredArrow L (R.obj b))).str =?= ?m.80 + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.80 : Category.{?u.121, u₁} + (CostructuredArrow L + (R.obj + b))) := ((Cat.of + (CostructuredArrow L (R.obj b))).str : Category.{u₁, u₁} ↑(Cat.of (CostructuredArrow L (R.obj b)))) + [Meta.isDefEq] ❌️ [instances] Category.{?u.121, u₁} + (CostructuredArrow L (R.obj b)) =?= Category.{u₁, u₁} ↑(Cat.of (CostructuredArrow L (R.obj b))) + [Meta.isDefEq] ❌️ [instances] CostructuredArrow L (R.obj b) =?= ↑(Cat.of (CostructuredArrow L (R.obj b))) + [Meta.isDefEq] ❌️ [instances] CostructuredArrow L + (R.obj b) =?= (Cat.of (CostructuredArrow L (R.obj b))).1 + [Meta.isDefEq.onFailure] ❌️ CostructuredArrow L + (R.obj b) =?= (Cat.of (CostructuredArrow L (R.obj b))).1 + [Meta.isDefEq.onFailure] ❌️ Category.{?u.121, u₁} + (CostructuredArrow L (R.obj b)) =?= Category.{u₁, u₁} ↑(Cat.of (CostructuredArrow L (R.obj b))) + [Meta.synthInstance] ✅️ Category.{u₁, u₁} (CostructuredArrow L (R.obj b)) (truncated) + [Meta.isDefEq] ❌️ [instances] (Cat.of + (CostructuredArrow L (R.obj b))).str =?= instCategoryCostructuredArrow_1 L (R.obj b) (truncated) + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.80 : Category.{?u.121, u₁} + (CostructuredArrow L + (R.obj + b))) := ((Cat.of + (CostructuredArrow L (R.obj b))).2 : Category.{u₁, u₁} (Cat.of (CostructuredArrow L (R.obj b))).1) + [Meta.isDefEq] ❌️ [instances] Category.{?u.121, u₁} + (CostructuredArrow L (R.obj b)) =?= Category.{u₁, u₁} (Cat.of (CostructuredArrow L (R.obj b))).1 + [Meta.isDefEq] ❌️ [instances] CostructuredArrow L (R.obj b) =?= (Cat.of (CostructuredArrow L (R.obj b))).1 + [Meta.isDefEq.onFailure] ❌️ CostructuredArrow L (R.obj b) =?= (Cat.of (CostructuredArrow L (R.obj b))).1 + [Meta.isDefEq.onFailure] ❌️ Category.{?u.121, u₁} + (CostructuredArrow L (R.obj b)) =?= Category.{u₁, u₁} (Cat.of (CostructuredArrow L (R.obj b))).1 + [Meta.synthInstance] ✅️ Category.{u₁, u₁} (CostructuredArrow L (R.obj b)) (truncated) + [Meta.isDefEq] ❌️ [instances] (Cat.of + (CostructuredArrow L (R.obj b))).2 =?= instCategoryCostructuredArrow_1 L (R.obj b) (truncated) +-/ +#guard_msgs in +postprocess_traces + filterSubtrees (fun x => (ofClass `Meta.synthInstance.apply x) <&&> + containsString "Types.hasColimitsOfShape" x) + >=> filterSubtrees (fun x => (ofClass `Meta.isDefEq.assign.checkTypes x) <&&> failed x) + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> succeeded x) + >=> elideBelow (fun x => (ofClass `Meta.isDefEq x) <&&> + containsString "instCategoryCostructuredArrow_1" x) +in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option backward.defeqAttrib.useBackward true in +set_option backward.isDefEq.respectTransparency false in +example (L : A ⥤ T) (R : B ⥤ T) + [IsFiltered B] [Final R] [∀ b, IsFiltered (CostructuredArrow L (R.obj b))] : IsFiltered A := by + refine isFiltered_of_nonempty_limit_colimit_to_colimit_limit fun J {_ _} F => ⟨?_⟩ + haveI : ∀ b, PreservesLimitsOfShape J + (colim (J := (R ⋙ CostructuredArrow.functor L).obj b) (C := Type u₁)) := fun b => by + simp only [comp_obj, CostructuredArrow.functor_obj, Cat.of_α] + set_option trace.Meta.synthInstance true in + set_option trace.Meta.isDefEq true in + set_option trace.Meta.isDefEq.printTransparency true in + set_option trace.Meta.isDefEq.assign.checkTypes true in + exact filtered_colim_preservesFiniteLimits + sorry + +/-! # Fix -/ + +theorem Cat.of_str {C} [inst : Category C] : (Cat.of C).str = inst := rfl + +-- Adding `Cat.of_str` to the `simp only` set rewrites the desynced `colim` `Category` instance back +-- to `CostructuredArrow`'s own `instCategoryCostructuredArrow_1`, realigning carrier and instance +-- so that `HasColimitsOfShape` synthesis needs no cross-boundary assignment. +set_option backward.isDefEq.instanceTypes "markOrSynth" in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in private lemma isFiltered_of_isFiltered_costructuredArrow_small (L : A ⥤ T) (R : B ⥤ T) @@ -42,7 +148,7 @@ private lemma isFiltered_of_isFiltered_costructuredArrow_small (L : A ⥤ T) (R let R' := Grothendieck.pre (CostructuredArrow.functor L) R haveI : ∀ b, PreservesLimitsOfShape J (colim (J := (R ⋙ CostructuredArrow.functor L).obj b) (C := Type u₁)) := fun b => by - simp only [comp_obj, CostructuredArrow.functor_obj, Cat.of_α] + simp only [comp_obj, CostructuredArrow.functor_obj, Cat.of_α, Cat.of_str] -- Added: `Cat.of_str` exact filtered_colim_preservesFiniteLimits refine lim.map ((colimitIsoColimitGrothendieck L F.flip).hom ≫ (inv (colimit.pre (CostructuredArrow.grothendieckProj L ⋙ F.flip) R'))) ≫ diff --git a/mathlib4/Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean b/mathlib4/Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean index 8bf1e8969..40deb03d6 100644 --- a/mathlib4/Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean +++ b/mathlib4/Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean @@ -32,7 +32,6 @@ Show the analogous results for functors which reflect or create (co)limits. @[expose] public section - open CategoryTheory open Opposite diff --git a/mathlib4/Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean b/mathlib4/Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean index 97112b1dc..fba2bffd3 100644 --- a/mathlib4/Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean +++ b/mathlib4/Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean @@ -13,6 +13,8 @@ public import Mathlib.AlgebraicTopology.RelativeCellComplex.Basic public import Mathlib.SetTheory.Cardinal.Regular public import Mathlib.CategoryTheory.MorphismProperty.Factorization +meta import Lean.PostprocessTraces + /-! # Cardinals that are suitable for the small object argument @@ -155,6 +157,10 @@ isomorphisms on the right side. -/ def propArrow : MorphismProperty (Arrow C) := fun _ _ f ↦ (coproducts.{w} I).pushouts f.left ∧ (isomorphisms C) f.right +/-! # Issue (Low Severity) -/ + +-- Works with "markOrSynth" if `Arrow` and `Arrow.Hom` are made implicit-reducible. +set_option backward.isDefEq.instanceTypes "none" in set_option backward.isDefEq.respectTransparency.types false in set_option backward.defeqAttrib.useBackward true in lemma succStruct_prop_le_propArrow : @@ -172,6 +178,114 @@ lemma succStruct_prop_le_propArrow : dsimp [succStruct] infer_instance +/-! ## Explanation -/ + +-- The opening `intro _ _ _ ⟨F⟩ f` destructures `(succStruct I κ).prop f✝`, which unfolds to an +-- `ofHoms` whose carrier `Arrow C ⥤ Arrow C` is exposed as `Comma (𝟭 C) (𝟭 C) ⥤ Comma (𝟭 C) (𝟭 C)`. +-- The `⟨F⟩` pattern re-elaborates `ofHoms.mk F`, and its `Functor.category` instance needs the base +-- `[Category (Arrow C)]`; that becomes an instance-typed mvar whose type is read off the goal at +-- the `Comma (𝟭 C) (𝟭 C)` spelling. The candidate `instCategoryArrow` (spelled at the `Arrow` +-- synonym) is rejected (trace below): the direct `.instances` check can't cross +-- `Comma (𝟭 C) (𝟭 C) =?= Arrow C` +-- (`Arrow` is a plain semireducible `def`), and under `markOrSynth` the re-synthesis fallback finds +-- `commaCategory`, which is not defeq to `instCategoryArrow` at `.instances` either. So the mvar is +-- never solved and `ofHoms.mk F` fails to unify. Same `Comma`/`Arrow`-vs-`Cat.of` carrier boundary +-- as `Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean`, here introduced by destructuring +-- rather than a `simp only`. + +section InstanceTypesDemo + +open Lean.PostprocessTraces + +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +set_option linter.style.longLine false in +/-- +error: Type mismatch + ofHoms.mk F +has type + ofHoms ?m.69 (?m.69 F) +but is expected to have type + (succStruct I κ).prop f✝ +--- +error: No goals to be solved +--- +trace: [Meta.synthInstance] ❌️ Category.{max u v, max u v} (Comma (𝟭 C) (𝟭 C) ⥤ Comma (𝟭 C) (𝟭 C)) + [Meta.synthInstance.apply] ❌️ apply @Functor.category to Category.{max u v, max u v} + (Comma (𝟭 C) (𝟭 C) ⥤ Comma (𝟭 C) (𝟭 C)) + [Meta.synthInstance.tryResolve] ❌️ Category.{max u v, max u v} + (Comma (𝟭 C) (𝟭 C) ⥤ + Comma (𝟭 C) (𝟭 C)) ≟ Category.{max ?u.61 ?u.60, max (max (max ?u.62 ?u.61) ?u.60) ?u.59} (?m.74 ⥤ ?m.76) + [Meta.isDefEq] ❌️ [instances] Category.{max u v, max u v} + (Comma (𝟭 C) (𝟭 C) ⥤ + Comma (𝟭 C) (𝟭 C)) =?= Category.{max ?u.61 ?u.60, max (max (max ?u.62 ?u.61) ?u.60) ?u.59} (?m.74 ⥤ ?m.76) + [Meta.isDefEq] ❌️ [instances] Comma (𝟭 C) (𝟭 C) ⥤ Comma (𝟭 C) (𝟭 C) =?= ?m.74 ⥤ ?m.76 + [Meta.isDefEq] ❌️ [implicit] instCategoryArrow =?= ?m.75 + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.75 : Category.{?u.59, max u v} + (Comma (𝟭 C) (𝟭 C))) := (instCategoryArrow : Category.{v, max u v} (Arrow C)) + [Meta.isDefEq] ❌️ [instances] Category.{?u.59, max u v} + (Comma (𝟭 C) (𝟭 C)) =?= Category.{v, max u v} (Arrow C) + [Meta.isDefEq] ❌️ [instances] Comma (𝟭 C) (𝟭 C) =?= Arrow C + [Meta.isDefEq] ❌️ [instances] @Comma =?= Arrow + [Meta.isDefEq.onFailure] ❌️ Comma (𝟭 C) (𝟭 C) =?= Arrow C + [Meta.isDefEq.onFailure] ❌️ Category.{?u.59, max u v} + (Comma (𝟭 C) (𝟭 C)) =?= Category.{v, max u v} (Arrow C) + [Meta.synthInstance] ✅️ Category.{v, max u v} (Comma (𝟭 C) (𝟭 C)) (truncated) + [Meta.isDefEq] ❌️ [implicit] instCategoryArrow =?= commaCategory (truncated) + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.75 : Category.{?u.59, max u v} + (Comma (𝟭 C) + (𝟭 + C))) := ({ toQuiver := instQuiverArrow, id := instCategoryArrow._aux_1, + comp := @instCategoryArrow._aux_3 C inst✝³, id_comp := ⋯, comp_id := ⋯, + assoc := ⋯ } : Category.{v, max u v} (Arrow C)) + [Meta.isDefEq] ❌️ [instances] Category.{?u.59, max u v} + (Comma (𝟭 C) (𝟭 C)) =?= Category.{v, max u v} (Arrow C) + [Meta.isDefEq] ❌️ [instances] Comma (𝟭 C) (𝟭 C) =?= Arrow C + [Meta.isDefEq] ❌️ [instances] @Comma =?= Arrow + [Meta.isDefEq.onFailure] ❌️ Comma (𝟭 C) (𝟭 C) =?= Arrow C + [Meta.isDefEq.onFailure] ❌️ Category.{?u.59, max u v} + (Comma (𝟭 C) (𝟭 C)) =?= Category.{v, max u v} (Arrow C) + [Meta.synthInstance] ✅️ Category.{v, max u v} (Comma (𝟭 C) (𝟭 C)) (truncated) + [Meta.isDefEq] ❌️ [implicit] { toQuiver := instQuiverArrow, id := instCategoryArrow._aux_1, + comp := @instCategoryArrow._aux_3 C inst✝³, id_comp := ⋯, comp_id := ⋯, + assoc := ⋯ } =?= commaCategory (truncated) +-/ +#guard_msgs in +postprocess_traces + filterSubtrees (fun x => (ofClass `Meta.synthInstance.apply x) <&&> + containsString "Functor.category" x) + >=> filterSubtrees (fun x => (ofClass `Meta.isDefEq.assign.checkTypes x) <&&> failed x) + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> succeeded x) + >=> elideBelow (fun x => (ofClass `Meta.isDefEq x) <&&> containsString "commaCategory" x) +in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option backward.isDefEq.respectTransparency.types false in +set_option backward.defeqAttrib.useBackward true in +example : + (succStruct I κ).prop ≤ (propArrow.{w} I).functorCategory (Arrow C) := by + have := locallySmall I κ + have := isSmall I κ + have := hasColimitsOfShape_discrete I κ + have := hasPushouts I κ + set_option trace.Meta.synthInstance true in + set_option trace.Meta.isDefEq true in + set_option trace.Meta.isDefEq.printTransparency true in + set_option trace.Meta.isDefEq.assign.checkTypes true in + intro _ _ _ ⟨F⟩ f + all_goals sorry + +end InstanceTypesDemo + /-- The functor `κ.ord.ToType ⥤ Arrow C ⥤ Arrow C` corresponding to the iterations of the successor structure `succStruct I κ`. -/ noncomputable def iterationFunctor : κ.ord.ToType ⥤ Arrow C ⥤ Arrow C := diff --git a/mathlib4/Mathlib/Condensed/TopCatAdjunction.lean b/mathlib4/Mathlib/Condensed/TopCatAdjunction.lean index e5935ba38..417aae16a 100644 --- a/mathlib4/Mathlib/Condensed/TopCatAdjunction.lean +++ b/mathlib4/Mathlib/Condensed/TopCatAdjunction.lean @@ -7,6 +7,7 @@ module public import Mathlib.Condensed.TopComparison public import Mathlib.Topology.Category.CompactlyGenerated +meta import Lean.PostprocessTraces /-! # The adjunction between condensed sets and topological spaces @@ -19,8 +20,12 @@ The counit is an isomorphism for compactly generated spaces, and we conclude tha `topCatToCondensedSet` is fully faithful when restricted to compactly generated spaces. -/ +set_option backward.isDefEq.instanceTypes "mark" + @[expose] public section +open Lean.PostprocessTraces + universe u open Condensed CondensedSet CategoryTheory CompHaus @@ -91,15 +96,155 @@ noncomputable def topCatAdjunctionCounit (X : TopCat.{u + 1}) : X.toCondensedSet rw [continuous_coinduced_dom] continuity } +-- The dual of `filterSubtrees`: drop matching subtrees (used to remove `onFailure` duplicates). +private meta partial def dropSubtrees (p : TracePattern) : TracePostprocessor := + fun trees => trees.filterMapM go +where + go (t : TraceTree) : Lean.CoreM (Option TraceTree) := do + if ← p t then + return none + match t with + | .leaf msg => return some (.leaf msg) + | .node data msg children wrap => return some (.node data msg (← children.filterMapM go) wrap) + +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +/-! # Issue (Medium Severity) -/ + set_option backward.isDefEq.respectTransparency.types false in +set_option backward.isDefEq.instanceTypes "none" in /-- `simp`-normal form of the lemma that `@[simps]` would generate. -/ @[simp] lemma topCatAdjunctionCounit_hom_apply (X : TopCat) (x) : -- We have to specify here to not infer the `TopologicalSpace` instance on `C(PUnit, X)`, -- which suggests type synonyms are being unfolded too far somewhere. + DFunLike.coe (F := @ContinuousMap C(PUnit, X) X (_) _) + (TopCat.Hom.hom (topCatAdjunctionCounit X)) x = + (x PUnit.unit : TopCat.carrier X) := rfl + +/-! +# Explanation + +Summary of the investigation: +* This lemma explicitly requires non-canonical topologies on spaces of continuous maps. +* Possible workaround: Give the instance explicitly. +* Question: Is this lemma's signature actually useful in this form? It seems to be unused. +-/ + +set_option linter.style.longLine false in +/-- +error: failed to synthesize instance of type class + DFunLike C(C(PUnit.{?u.16 + 1}, ↑X), ↑X) ?m.1 ?m.7 +--- +error: Function expected at + x +but this term has type + ?m.1 + +Note: Expected a function because this term is being applied to the argument + PUnit.unit +--- +trace: [Meta.synthInstance] ❌️ DFunLike C(C(PUnit.{?u.16 + 1}, ↑X), ↑X) ?m.1 ?m.7 + [Meta.synthInstance.apply] ❌️ apply @ContinuousMap.instFunLike to DFunLike C(C(PUnit.{?u.16 + 1}, ↑X), ↑X) ?m.11 ?m.12 + [Meta.synthInstance.tryResolve] ❌️ DFunLike C(C(PUnit.{?u.16 + 1}, ↑X), ↑X) ?m.11 + ?m.12 ≟ DFunLike C(?m.14, ?m.15) ?m.14 fun x ↦ ?m.15 + [Meta.isDefEq] ❌️ [instances] DFunLike C(C(PUnit.{?u.16 + 1}, ↑X), ↑X) ?m.11 + ?m.12 =?= DFunLike C(?m.14, ?m.15) ?m.14 fun x ↦ ?m.15 + [Meta.isDefEq] ❌️ [instances] C(C(PUnit.{?u.16 + 1}, ↑X), ↑X) =?= C(?m.14, ?m.15) + [Meta.isDefEq] ❌️ [implicit] X.toCondensedSet.toTopCat.str =?= ?m.16 + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.16 : TopologicalSpace + C(PUnit.{?u.16 + 1}, + ↑X)) := (X.toCondensedSet.toTopCat.str : TopologicalSpace ↑X.toCondensedSet.toTopCat) + [Meta.isDefEq] ❌️ [instances] TopologicalSpace + C(PUnit.{?u.16 + 1}, ↑X) =?= TopologicalSpace ↑X.toCondensedSet.toTopCat + [Meta.isDefEq] ❌️ [instances] C(PUnit.{?u.16 + 1}, ↑X) =?= ↑X.toCondensedSet.toTopCat + [Meta.isDefEq] ❌️ [instances] C(PUnit.{?u.16 + 1}, ↑X) =?= X.toCondensedSet.toTopCat.1 + [Meta.isDefEq] ❌️ [instances] C(PUnit.{?u.16 + 1}, + ↑X) =?= X.toCondensedSet.obj.obj (Opposite.op (of PUnit.{?u.16 + 1})) + [Meta.isDefEq] ❌️ [instances] C(PUnit.{?u.16 + 1}, + ↑X) =?= X.toCondensedSet.obj.1 (Opposite.op (of PUnit.{?u.16 + 1})) + [Meta.isDefEq] ❌️ [instances] ContinuousMap =?= X.toCondensedSet.obj.1 + [Meta.isDefEq.onFailure] ❌️ ContinuousMap =?= X.toCondensedSet.obj.1 + [Meta.isDefEq.onFailure] ❌️ C(PUnit.{?u.16 + 1}, + ↑X) =?= X.toCondensedSet.obj.1 (Opposite.op (of PUnit.{?u.16 + 1})) + [Meta.isDefEq.onFailure] ❌️ TopologicalSpace + C(PUnit.{?u.16 + 1}, ↑X) =?= TopologicalSpace ↑X.toCondensedSet.toTopCat + [Meta.synthInstance] ✅️ TopologicalSpace C(PUnit.{?u.16 + 1}, ↑X) (truncated) + [Meta.isDefEq] ❌️ [implicit] X.toCondensedSet.toTopCat.str =?= ContinuousMap.compactOpen (truncated) + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.16 : TopologicalSpace + C(PUnit.{?u.16 + 1}, + ↑X)) := ({ IsOpen := fun s ↦ IsOpen (X.toCondensedSet.coinducingCoprod ⁻¹' s), isOpen_univ := ⋯, + isOpen_inter := ⋯, + isOpen_sUnion := + ⋯ } : TopologicalSpace (X.toCondensedSet.obj.obj (Opposite.op (of PUnit.{?u.16 + 1})))) (truncated) +-/ +#guard_msgs in +postprocess_traces + filterSubtrees (fun x => (ofClass `Meta.synthInstance.apply x) <&&> + (containsString "ContinuousMap.instFunLike" x)) + >=> filterSubtrees (fun x => ofClass `Meta.isDefEq.assign.checkTypes x <&&> failed x) + >=> elideBelow (fun x => ofClass `Meta.synthInstance x <&&> succeeded x) + >=> elideBelow (fun x => ofClass `Meta.isDefEq x <&&> containsString "ContinuousMap.compactOpen" x) + >=> elideBelow (fun x => ofClass `Meta.isDefEq.assign.checkTypes x <&&> containsString ":= ({" x) +in +set_option trace.Meta.synthInstance true in +set_option trace.Meta.isDefEq true in +set_option trace.Meta.isDefEq.printTransparency true in +set_option trace.Meta.isDefEq.assign.checkTypes true in +set_option backward.isDefEq.respectTransparency.types false in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +example (X : TopCat) (x) : DFunLike.coe (F := @ContinuousMap C(PUnit, X) X (_) _) (TopCat.Hom.hom (topCatAdjunctionCounit X)) x = x PUnit.unit := rfl +section +variable (X : TopCat.{u + 1}) + +/-- +error: Tactic `rfl` failed: The left-hand side + X.toCondensedSet.toTopCat.str +is not definitionally equal to the right-hand side + ContinuousMap.compactOpen + +X✝¹ : CondensedSet +X✝ X : TopCat +⊢ X.toCondensedSet.toTopCat.str = ContinuousMap.compactOpen +-/ +#guard_msgs in +example (X : TopCat.{u + 1}) : + X.toCondensedSet.toTopCat.str = + (ContinuousMap.compactOpen : TopologicalSpace C(PUnit, X)) := by + apply_rfl + +end + + +/-! # Fix -/ +/- +Potential fix: explicitly annotate `x`, making the synthesis succeed without the `F` annotation. +This changes the `F` value, though, and this affects the discrimination key. +It's a very significant change, but I can't tell which version has the correct signature. +-/ +set_option backward.isDefEq.respectTransparency.types false in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +/-- `simp`-normal form of the lemma that `@[simps]` would generate. -/ +@[simp] lemma topCatAdjunctionCounit_hom_apply_fixed? (X : TopCat) (x : C(PUnit, X)) : + -- We have to specify here to not infer the `TopologicalSpace` instance on `C(PUnit, X)`, + -- which suggests type synonyms are being unfolded too far somewhere. + DFunLike.coe + (TopCat.Hom.hom (topCatAdjunctionCounit X)) x = + (x PUnit.unit : TopCat.carrier X) := rfl + set_option backward.isDefEq.respectTransparency.types false in /-- The counit of the adjunction `condensedSetToTopCat ⊣ topCatToCondensedSet` is always bijective, but not an isomorphism in general (the inverse isn't continuous unless `X` is compactly generated). diff --git a/mathlib4/Mathlib/FieldTheory/Galois/Profinite.lean b/mathlib4/Mathlib/FieldTheory/Galois/Profinite.lean index 1fa9e055d..c70fef4fd 100644 --- a/mathlib4/Mathlib/FieldTheory/Galois/Profinite.lean +++ b/mathlib4/Mathlib/FieldTheory/Galois/Profinite.lean @@ -9,6 +9,8 @@ public import Mathlib.FieldTheory.KrullTopology public import Mathlib.FieldTheory.Galois.GaloisClosure public import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic +meta import Lean.PostprocessTraces + /-! # Galois Group as a profinite group @@ -53,6 +55,10 @@ In a field extension `K/k` -/ +set_option backward.isDefEq.instanceTypes "mark" + +open Lean.PostprocessTraces + @[expose] public section open CategoryTheory Opposite @@ -295,6 +301,9 @@ lemma krullTopology_mem_nhds_one_iff_of_isGalois [IsGalois k K] (A : Set Gal(K/k exact ⟨fun ⟨L, _, hL, hsub⟩ ↦ ⟨{ toIntermediateField := L, isGalois := ⟨⟩ }, hsub⟩, fun ⟨L, hL⟩ ↦ ⟨L, inferInstance, inferInstance, hL⟩⟩ +/-! # Issue -/ + +set_option backward.isDefEq.instanceTypes "markOrSynth" in lemma isOpen_mulEquivToLimit_image_fixingSubgroup [IsGalois k K] (L : FiniteGaloisIntermediateField k K) : IsOpen (mulEquivToLimit k K '' L.fixingSubgroup) := by let fix1 : Set (Π L, (asProfiniteGaloisGroupFunctor k K).obj L) := {f | f (op L) = 1} @@ -305,6 +314,119 @@ lemma isOpen_mulEquivToLimit_image_fixingSubgroup [IsGalois k K] obtain ⟨σ, rfl⟩ := (mulEquivToLimit k K).surjective x simpa using! FiniteGaloisIntermediateField.mem_fixingSubgroup_iff σ L +/-! ## Explanation + +The final `simpa` rewrites with `EmbeddingLike.apply_eq_iff_eq`, triggering synthesis of +`EmbeddingLike (Gal(K/k) ≃* ↥(limitConePtAux …)) …` via `MulEquiv.instEquivLike`. Unifying the +candidate's conclusion assigns the instance-typed `?inst : Mul ↥(limitConePtAux …)` from the goal's +`≃*` type; the direct check `Mul ↥(…) =?= Mul ↥(…)` fails at `.instances` because the two `↥` +carriers hide the ambient product group at two spellings — +`(forget₂ FiniteGrp ProfiniteGrp).obj ((finGaloisGroupFunctor k K).obj j)` vs +`(asProfiniteGaloisGroupFunctor k K).obj j` — whose reconciliation needs the `Functor.comp` delta +that `.instances` does not provide (it stalls at +`ofFiniteGrp =?= (asProfiniteGaloisGroupFunctor k K).1`). +Under `"markOrSynth"` the mvar is re-synthesized at its own type — `#synth` below shows it returns +exactly the rejected `(limitConePtAux …).mul` — and the following unification succeeds at +`.implicit`, where `Functor.comp` unfolds. Same hidden-index pattern as +`Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean`; the rejected mvar is data-valued (`Mul`). +-/ + +-- The instance that the toolchain rejects is exactly what instance synthesis returns for the +-- mvar's type. +/-- info: (limitConePtAux (asProfiniteGaloisGroupFunctor k K)).mul -/ +#guard_msgs in +#synth Mul ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)) + +private meta partial def dropSubtrees (p : TracePattern) : TracePostprocessor := + fun trees => trees.filterMapM go +where + go (t : TraceTree) : Lean.CoreM (Option TraceTree) := do + if ← p t then + return none + match t with + | .leaf msg => return some (.leaf msg) + | .node data msg children wrap => return some (.node data msg (← children.filterMapM go) wrap) + +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +set_option linter.style.longLine false in +/-- +trace: [Meta.synthInstance] ✅️ EmbeddingLike (Gal(K/k) ≃* ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) Gal(K/k) + ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)) + [Meta.synthInstance.apply] ✅️ apply @MulEquiv.instEquivLike to EquivLike + (Gal(K/k) ≃* ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) Gal(K/k) + ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)) + [Meta.synthInstance.tryResolve] ✅️ EquivLike (Gal(K/k) ≃* ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) + Gal(K/k) + ↥(limitConePtAux + (asProfiniteGaloisGroupFunctor k + K)) ≟ EquivLike (Gal(K/k) ≃* ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) Gal(K/k) + ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)) + [Meta.isDefEq] ✅️ [instances] EquivLike (Gal(K/k) ≃* ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) ?m.131 + ?m.132 =?= EquivLike (?m.134 ≃* ?m.135) ?m.134 ?m.135 + [Meta.isDefEq] ✅️ [instances] Gal(K/k) ≃* + ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)) =?= ?m.134 ≃* ?m.135 + [Meta.isDefEq] ✅️ [implicit] (limitConePtAux (asProfiniteGaloisGroupFunctor k K)).mul =?= ?m.137 + [Meta.isDefEq] (limitConePtAux + (asProfiniteGaloisGroupFunctor k K)).mul [nonassignable] =?= ?m.137 [assignable] + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.137 : Mul + ↥(limitConePtAux + (asProfiniteGaloisGroupFunctor k + K))) := ((limitConePtAux + (asProfiniteGaloisGroupFunctor k + K)).mul : Mul ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) + [Meta.isDefEq] ❌️ [instances] Mul + ↥(limitConePtAux + (asProfiniteGaloisGroupFunctor k + K)) =?= Mul ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)) (truncated) + [Meta.synthInstance] ✅️ Mul ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)) (truncated) + [Meta.isDefEq] ✅️ [implicit] (limitConePtAux + (asProfiniteGaloisGroupFunctor k + K)).mul =?= (limitConePtAux (asProfiniteGaloisGroupFunctor k K)).mul (truncated) +-/ +#guard_msgs in +postprocess_traces + filterSubtrees (fun x => (ofClass `Meta.synthInstance x) <&&> + (containsString "EmbeddingLike" x) <&&> succeeded x) + >=> filterSubtrees (fun x => (ofClass `Meta.isDefEq x) <&&> (containsString ".mul =?= ?m" x)) + >=> dropSubtrees (ofClass `Meta.isDefEq.onFailure) + >=> elideBelow (fun x => (failed x) <&&> (containsString "Mul" x)) + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) + <&&> (do return !(← containsString "EmbeddingLike" x))) + >=> elideBelow (fun x => (containsString "[implicit]" x) + <&&> (do return !(← containsString "?m" x))) +in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option trace.Meta.synthInstance true in +set_option trace.Meta.isDefEq true in +set_option trace.Meta.isDefEq.printTransparency true in +set_option trace.Meta.isDefEq.assign.checkTypes true in +example [IsGalois k K] (L : FiniteGaloisIntermediateField k K) : + IsOpen (mulEquivToLimit k K '' L.fixingSubgroup) := by + let fix1 : Set (Π L, (asProfiniteGaloisGroupFunctor k K).obj L) := {f | f (op L) = 1} + suffices mulEquivToLimit k K '' L.1.fixingSubgroup = Set.preimage Subtype.val fix1 by + rw [this] + exact (isOpen_induced <| (continuous_apply (op L)).isOpen_preimage {1} trivial) + ext x + obtain ⟨σ, rfl⟩ := (mulEquivToLimit k K).surjective x + simpa using! FiniteGaloisIntermediateField.mem_fixingSubgroup_iff σ L + +-- Same root cause as `isOpen_mulEquivToLimit_image_fixingSubgroup` above (see the explanation +-- there): the `simp only [krullTopology_mem_nhds_one_iff_of_isGalois, …]` and the reference to +-- that lemma again unify the bundled group structure of the limit cone point at `.instances`, +-- rescued by re-synthesis under `"markOrSynth"`. Here the decisively rejected instance is +-- `Pi.group` for the ambient product group. +set_option backward.isDefEq.instanceTypes "markOrSynth" in lemma mulEquivToLimit_symm_continuous [IsGalois k K] : Continuous (mulEquivToLimit k K).symm := by apply continuous_of_continuousAt_one _ (continuousAt_def.mpr _) simp only [map_one, krullTopology_mem_nhds_one_iff_of_isGalois, ← MulEquiv.coe_toEquiv_symm, diff --git a/mathlib4/Mathlib/Geometry/Manifold/Instances/Sphere.lean b/mathlib4/Mathlib/Geometry/Manifold/Instances/Sphere.lean index ea27f5a75..d846b47de 100644 --- a/mathlib4/Mathlib/Geometry/Manifold/Instances/Sphere.lean +++ b/mathlib4/Mathlib/Geometry/Manifold/Instances/Sphere.lean @@ -16,6 +16,7 @@ public import Mathlib.Geometry.Manifold.Instances.Real public import Mathlib.Geometry.Manifold.MFDeriv.Basic public import Mathlib.LinearAlgebra.Complex.FiniteDimensional public import Mathlib.Tactic.Module +meta import Lean.PostprocessTraces /-! # Manifold structure on the sphere @@ -66,6 +67,8 @@ naive expression `EuclideanSpace ℝ (Fin (finrank ℝ E - 1))` for the model sp Relate the stereographic projection to the inversion of the space. -/ +set_option backward.isDefEq.instanceTypes "mark" + @[expose] public section @@ -473,6 +476,9 @@ theorem contMDiff_neg_sphere {m : ℕ∞ω} {n : ℕ} [Fact (finrank ℝ E = n + apply contDiff_neg.contMDiff.comp _ exact contMDiff_coe_sphere +/-! # Issue -/ + +set_option backward.isDefEq.instanceTypes "markOrSynth" in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in private lemma stereographic'_neg {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1) : @@ -481,7 +487,105 @@ private lemma stereographic'_neg {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : s simp only [EmbeddingLike.map_eq_zero_iff] apply stereographic_neg_apply +/-! ## Explanation -/ + +open Lean.PostprocessTraces + +-- All three sites share one spelling desync: `coe_neg_sphere : ↑(-v) = -↑v` is `rfl` at default +-- transparency (the sphere's `Neg` is `Subtype.map Neg.neg _`), but the two spellings are NOT +-- defeq at `.instances`. Rewriting with it (a simp lemma, also in `mfld_simps`) desyncs type +-- indices (rewritten to `-↑v`) from instance arguments inside the term (still typed at `↑(-v)`). +-- Here, after `dsimp [stereographic']`, `simp only [EmbeddingLike.map_eq_zero_iff]` synthesizes the +-- `≃ₗᵢ`'s `EquivLike`, whose `LinearIsometryEquiv.instEquivLike` candidate reads the carrier +-- `↥(ℝ ∙ -↑v)ᗮ` off the type and leaves an instance-typed `SeminormedAddCommGroup ↥(ℝ ∙ -↑v)ᗮ` mvar +-- that has to swallow the old-spelling `↥(ℝ ∙ ↑(-v))ᗮ`-typed value. The direct `.instances` check +-- fails (`-↑v =?= ↑(-v)` stalls); `"mark"` would reject and the simp lemma would never apply +-- ("`simp` made no progress") — `"markOrSynth"` re-synthesizes at `↥(ℝ ∙ -↑v)ᗮ` and unifies, +-- rescuing the rewrite. The `E ↔ TangentSpace` defeq abuse these proofs are known for is guarded by +-- the adjacent `respectTransparency false`; this `instanceTypes` site is the sphere-coercion +-- desync. + +-- `coe_neg_sphere` is `rfl` at default transparency, but not at `.instances`. +example (v : sphere (0 : E) 1) : (↑(-v) : E) = -↑v := rfl + +private meta partial def dropSubtrees (p : TracePattern) : TracePostprocessor := + fun trees => trees.filterMapM go +where + go (t : TraceTree) : Lean.CoreM (Option TraceTree) := do + if ← p t then + return none + match t with + | .leaf msg => return some (.leaf msg) + | .node data msg children wrap => return some (.node data msg (← children.filterMapM go) wrap) + +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +set_option linter.style.longLine false in +/-- +trace: [Meta.synthInstance] ✅️ EmbeddingLike (↥(ℝ ∙ -↑v)ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n)) (↥(ℝ ∙ -↑v)ᗮ) + (EuclideanSpace ℝ (Fin n)) + [Meta.synthInstance.apply] ✅️ apply @LinearIsometryEquiv.instEquivLike to EquivLike + (↥(ℝ ∙ -↑v)ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n)) (↥(ℝ ∙ -↑v)ᗮ) (EuclideanSpace ℝ (Fin n)) + [Meta.synthInstance.tryResolve] ✅️ EquivLike (↥(ℝ ∙ -↑v)ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n)) (↥(ℝ ∙ -↑v)ᗮ) + (EuclideanSpace ℝ + (Fin n)) ≟ EquivLike (↥(ℝ ∙ -↑v)ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n)) (↥(ℝ ∙ -↑v)ᗮ) (EuclideanSpace ℝ (Fin n)) + [Meta.isDefEq] ✅️ [instances] EquivLike (↥(ℝ ∙ -↑v)ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n)) ?m.64 + ?m.65 =?= EquivLike (?m.69 ≃ₛₗᵢ[?m.73] ?m.70) ?m.69 ?m.70 + [Meta.isDefEq] ✅️ [instances] ↥(ℝ ∙ -↑v)ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) =?= ?m.69 ≃ₛₗᵢ[?m.73] ?m.70 + [Meta.isDefEq] ✅️ [instances] NormedAddCommGroup.toSeminormedAddCommGroup =?= ?m.77 + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.77 : SeminormedAddCommGroup + ↥(ℝ ∙ -↑v)ᗮ) := (NormedAddCommGroup.toSeminormedAddCommGroup : SeminormedAddCommGroup ↥(ℝ ∙ ↑(-v))ᗮ) + [Meta.isDefEq] ❌️ [instances] SeminormedAddCommGroup + ↥(ℝ ∙ -↑v)ᗮ =?= SeminormedAddCommGroup ↥(ℝ ∙ ↑(-v))ᗮ (truncated) + [Meta.synthInstance] ✅️ SeminormedAddCommGroup ↥(ℝ ∙ -↑v)ᗮ (truncated) + [Meta.isDefEq] ✅️ [instances] NormedAddCommGroup.toSeminormedAddCommGroup =?= (ℝ ∙ + -↑v)ᗮ.seminormedAddCommGroup (truncated) +--- +warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended for development and not for final code. If you intend to submit this contribution to the Mathlib project, please remove 'set_option trace.Meta.synthInstance'. + +Note: This linter can be disabled with `set_option linter.style.setOption false` +-/ +#guard_msgs in +postprocess_traces + dropSubtrees (fun x => (ofClass `Meta.synthInstance x) <&&> containsString "ZeroHomClass" x) + >=> filterSubtrees (fun x => (ofClass `Meta.isDefEq.assign.checkTypes x) + <&&> containsString "SeminormedAddCommGroup ↥(ℝ ∙ ↑(-v))ᗮ)" x) + >=> elideBelow (fun x => (ofClass `Meta.isDefEq x) <&&> failed x + <&&> containsString "SeminormedAddCommGroup ↥(ℝ ∙ -↑v)ᗮ =?= SeminormedAddCommGroup" x) + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> succeeded x + <&&> containsString "SeminormedAddCommGroup ↥(ℝ ∙ -↑v)ᗮ" x) + >=> elideBelow (fun x => (ofClass `Meta.isDefEq x) <&&> succeeded x + <&&> containsString "toSeminormedAddCommGroup =?= (ℝ ∙" x) +in +set_option backward.defeqAttrib.useBackward true in +set_option backward.isDefEq.respectTransparency false in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +example {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1) : + stereographic' n (-v) v = 0 := by + dsimp [stereographic'] + set_option trace.Meta.synthInstance true in + set_option trace.Meta.isDefEq true in + set_option trace.Meta.isDefEq.printTransparency true in + set_option trace.Meta.isDefEq.assign.checkTypes true in + simp only [EmbeddingLike.map_eq_zero_iff] + apply stereographic_neg_apply + +-- Same `coe_neg_sphere` desync as `stereographic'_neg`; here the inner `convert!` bridges the two +-- spellings with a cast and the closing `simp` hits the rejected assignment (rescued by +-- `"markOrSynth"`). See the Explanation above. (`convert!` rolls back its own traces, so the +-- decisive `checkTypes` shows up on the follow-up `simp`.) -- TODO: rephrase this using `mvfderiv`, avoiding the defeq abuse +set_option backward.isDefEq.instanceTypes "markOrSynth" in set_option backward.isDefEq.respectTransparency false in /-- Consider the differential of the inclusion of the sphere in `E` at the point `v` as a continuous linear map from `TangentSpace (𝓡 n) v` to `E`. The range of this map is the orthogonal complement @@ -523,7 +627,10 @@ theorem range_mfderiv_coe_sphere {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : s rw [Submodule.neg_mem_iff] exact Submodule.mem_span_singleton_self (v : E) +-- Same `coe_neg_sphere` desync as `stereographic'_neg`, via the inner `convert!` + closing `simp` +-- (rescued by `"markOrSynth"`). See the Explanation above. -- TODO: rephrase this using `mvfderiv`, avoiding the defeq abuse +set_option backward.isDefEq.instanceTypes "markOrSynth" in set_option backward.isDefEq.respectTransparency false in /-- Consider the differential of the inclusion of the sphere in `E` at the point `v` as a continuous linear map from `TangentSpace (𝓡 n) v` to `E`. This map is injective. -/ diff --git a/mathlib4/Mathlib/Geometry/Manifold/IsManifold/Basic.lean b/mathlib4/Mathlib/Geometry/Manifold/IsManifold/Basic.lean index 8e1ea40bb..800ae858e 100644 --- a/mathlib4/Mathlib/Geometry/Manifold/IsManifold/Basic.lean +++ b/mathlib4/Mathlib/Geometry/Manifold/IsManifold/Basic.lean @@ -1034,7 +1034,8 @@ set_option linter.unusedVariables false in The definition of `TangentSpace` is not reducible so that type class inference does not pick wrong instances. -/ -@[nolint unusedArguments, wikidata Q909601] +-- TODO: The `implicit_reducible` causes issues in `SpecificFunctions` and `MFDeriv.NormedSpace` +@[nolint unusedArguments, wikidata Q909601, implicit_reducible] def TangentSpace {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) diff --git a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean index fd47f4d3d..8e4604894 100644 --- a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean +++ b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean @@ -493,7 +493,12 @@ theorem writtenInExtChartAt_comp (h : ContinuousWithinAt f s x) : variable {f' f₀' f₁' : TangentSpace% x →L[𝕜] TangentSpace% (f x)} {g' : TangentSpace% (f x) →L[𝕜] TangentSpace% (g (f x))} -set_option backward.isDefEq.respectTransparency false in +/-! +# Issue + +Fixed by making `TangentSpace` implicit-reducible at its definition site. +-/ + /-- `UniqueMDiffWithinAt` achieves its goal: it implies the uniqueness of the derivative. -/ protected nonrec theorem UniqueMDiffWithinAt.eq (U : UniqueMDiffAt[s] x) (h : HasMFDerivAt[s] f x f') (h₁ : HasMFDerivAt[s] f x f₁') : f' = f₁' := by @@ -516,12 +521,10 @@ theorem mfderivWithin_univ : mfderiv[univ] f = mfderiv% f := by simp only [mfderivWithin, mfderiv, mfld_simps] rw [mdifferentiableWithinAt_univ] -set_option backward.isDefEq.respectTransparency false in theorem mfderivWithin_zero_of_not_mdifferentiableWithinAt (h : ¬MDiffAt[s] f x) : mfderiv[s] f x = 0 := by simp only [mfderivWithin, h, if_neg, not_false_iff] -set_option backward.isDefEq.respectTransparency false in theorem mfderiv_zero_of_not_mdifferentiableAt (h : ¬MDiffAt f x) : mfderiv% f x = 0 := by simp only [mfderiv, h, if_neg, not_false_iff] @@ -585,14 +588,12 @@ theorem hasMFDerivAt_unique (h₀ : HasMFDerivAt% f x f₀') (h₁ : HasMFDerivA rw [← hasMFDerivWithinAt_univ] at h₀ h₁ exact (uniqueMDiffWithinAt_univ I).eq h₀ h₁ -set_option backward.isDefEq.respectTransparency false in theorem hasMFDerivWithinAt_inter' (h : t ∈ 𝓝[s] x) : HasMFDerivAt[s ∩ t] f x f' ↔ HasMFDerivAt[s] f x f' := by rw [HasMFDerivWithinAt, HasMFDerivWithinAt, extChartAt_preimage_inter_eq, hasFDerivWithinAt_inter', continuousWithinAt_inter' h] exact extChartAt_preimage_mem_nhdsWithin h -set_option backward.isDefEq.respectTransparency false in theorem hasMFDerivWithinAt_inter (h : t ∈ 𝓝 x) : HasMFDerivAt[s ∩ t] f x f' ↔ HasMFDerivAt[s] f x f' := by rw [HasMFDerivWithinAt, HasMFDerivWithinAt, extChartAt_preimage_inter_eq, hasFDerivWithinAt_inter, diff --git a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean index 1112728ab..42244c794 100644 --- a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean +++ b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean @@ -524,6 +524,8 @@ lemma mvfderivWithin_neg {g : M → F} {x : M} (hs : UniqueMDiffAt[s] x) : simp [mvfderivWithin, mfderivWithin_neg hs] rfl +set_option allowUnsafeReducibility true in +attribute [local semireducible] TangentSpace in @[simp, to_fun mvfderivWithin_fun_smul] lemma mvfderivWithin_smul {a : M → 𝕜} (ha : MDiffAt[s] a x) {g : M → F} (hg : MDiffAt[s] g x) (hs : UniqueMDiffAt[s] x) : @@ -579,6 +581,8 @@ lemma mvfderiv_smul {x : M} {a : M → 𝕜} (ha : MDiffAt a x) {g : M → F} (h ext v simp [mvfderiv, -Pi.smul_apply', fromTangentSpace_mfderiv_smul_apply ha hg] +set_option allowUnsafeReducibility true in +attribute [local semireducible] TangentSpace in @[simp, to_fun mvfderiv_fun_mul] lemma mvfderiv_mul {f g : M → 𝕜} {x : M} (hf : MDiffAt f x) (hg : MDiffAt g x) : d% (f * g) x = f x • d% g x + (g x) • (d% f x) := by diff --git a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean index a3ba6c2a7..d0508a866 100644 --- a/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean +++ b/mathlib4/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean @@ -1104,6 +1104,8 @@ section Field variable {z : M} {F' : Type*} [NormedField F'] [NormedAlgebra 𝕜 F'] {p q : M → F'} {p' q' : TangentSpace% z →L[𝕜] F'} +set_option allowUnsafeReducibility true in +attribute [local semireducible] TangentSpace in set_option backward.isDefEq.respectTransparency.types false in lemma HasMFDerivWithinAt.inv (hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p') (hp_ne : p z ≠ 0) : HasMFDerivWithinAt I 𝓘(𝕜, F') (p⁻¹) s z (-(p z ^ 2)⁻¹ • p' : E →L[𝕜] F') := by diff --git a/mathlib4/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean b/mathlib4/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean index 2121cd479..4a2af4f8e 100644 --- a/mathlib4/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean +++ b/mathlib4/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean @@ -12,6 +12,8 @@ public import Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable public import Mathlib.Geometry.Manifold.VectorField.Pullback import Mathlib.Geometry.Manifold.Notation +meta import Lean.PostprocessTraces + /-! # Lie brackets of vector fields on manifolds @@ -27,6 +29,8 @@ The main results are the following: -/ +open Lean.PostprocessTraces + public section open Set Function Filter NormedSpace @@ -103,12 +107,22 @@ lemma mlieBracketWithin_eq_lieBracketWithin {V W : Π (x : E), TangentSpace 𝓘 @[simp] lemma mlieBracketWithin_univ : mlieBracketWithin I V W univ = mlieBracket I V W := (rfl) +/-! +# Issue (Low Severity) + +Can be fixed by making `TangentSpace` implicit-reducible at its definition site and then removing +`respectTransparency false`. +-/ + +set_option backward.isDefEq.instanceTypes "none" in set_option backward.isDefEq.respectTransparency false in lemma mlieBracketWithin_eq_zero_of_eq_zero (hV : V x = 0) (hW : W x = 0) : mlieBracketWithin I V W s x = 0 := by simp only [mlieBracketWithin, mpullback_apply] rw [lieBracketWithin_eq_zero_of_eq_zero] - · simp + · simp only [extChartAt, OpenPartialHomeomorph.extend, PartialEquiv.coe_trans, + ModelWithCorners.toPartialEquiv_coe, PartialHomeomorph.toFun_eq_coe, + OpenPartialHomeomorph.coe_toPartialHomeomorph, comp_apply, map_zero] · simp only [mpullbackWithin_apply] have : (extChartAt I x).symm ((extChartAt I x) x) = x := by simp rw [this, hV] @@ -135,6 +149,14 @@ lemma mlieBracket_swap_apply : mlieBracket I V W x = - mlieBracket I W V x := lemma mlieBracket_swap : mlieBracket I V W = - mlieBracket I W V := mlieBracketWithin_swap +/-! +# Issue (Low Severity) + +Can be fixed by making `TangentSpace` implicit-reducible at its definition site and then removing +`respectTransparency false`. +-/ + +set_option backward.isDefEq.instanceTypes "none" in set_option backward.isDefEq.respectTransparency false in @[simp] lemma mlieBracketWithin_self : mlieBracketWithin I V V = 0 := by ext x; simp [mlieBracketWithin, mpullback] @@ -335,7 +357,21 @@ private lemma mfderiv_extChart_inverse_comp_aux : ((mfderiv[range I] φ.symm (φ x)).inverse) (W (φ.symm (φ x))) = W x := by rw [mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm, extChartAt_to_inv] -set_option backward.isDefEq.respectTransparency false in +/-! +# Issue (High Severity) + + HSMul (TangentSpace 𝓘(𝕜,𝕜) (f x)) (TangentSpace I x) ?m.238 + └ @instHSMul ⇒ SMul + └ @SMulZeroClass.toSMul ⇒ SMulZeroClass + └ @SMulWithZero.toSMulZeroClass ⇒ SMulWithZero + └ MulActionWithZero.toSMulWithZero ⇒ MulActionWithZero + └ @Module.toMulActionWithZero ⇒ Module + +would probably work with HSMul 𝕜 (TangentSpace I x) ?m.238 +-/ + +set_option backward.isDefEq.instanceTypes "none" in +-- set_option backward.isDefEq.respectTransparency false in /-- Pulling back through `extChartAt` the scalar multiplication of a vector field by the derivative of a scalar function equals the scalar multiplication by the manifold derivative. -/ lemma mpullback_mfderivWithin_apply_smul {f : M → 𝕜} diff --git a/mathlib4/Mathlib/Geometry/Manifold/VectorField/Pullback.lean b/mathlib4/Mathlib/Geometry/Manifold/VectorField/Pullback.lean index c241e1f16..4d139cfa1 100644 --- a/mathlib4/Mathlib/Geometry/Manifold/VectorField/Pullback.lean +++ b/mathlib4/Mathlib/Geometry/Manifold/VectorField/Pullback.lean @@ -208,7 +208,7 @@ lemma mpullbackWithin_eq_pullbackWithin {f : E → E'} {V : E' → E'} {s : Set mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f V s = pullbackWithin 𝕜 f V s := by ext x simp only [mpullbackWithin, mfderivWithin_eq_fderivWithin, pullbackWithin] - rfl + -- rfl set_option backward.isDefEq.respectTransparency false in lemma mpullback_eq_pullback {f : E → E'} {V : E' → E'} : diff --git a/mathlib4/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/mathlib4/Mathlib/Geometry/RingedSpace/OpenImmersion.lean index cc16fc4c4..7f803142f 100644 --- a/mathlib4/Mathlib/Geometry/RingedSpace/OpenImmersion.lean +++ b/mathlib4/Mathlib/Geometry/RingedSpace/OpenImmersion.lean @@ -194,7 +194,6 @@ theorem inv_naturality {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) : TopCat.Presheaf.pushforward_obj_map] congr 1 -set_option backward.isDefEq.respectTransparency.types false in instance (U : Opens X) : IsIso (invApp f U) := by delta invApp; infer_instance set_option backward.isDefEq.respectTransparency.types false in diff --git a/mathlib4/Mathlib/LinearAlgebra/AffineSpace/Ordered.lean b/mathlib4/Mathlib/LinearAlgebra/AffineSpace/Ordered.lean index 48960c7e0..e792384e1 100644 --- a/mathlib4/Mathlib/LinearAlgebra/AffineSpace/Ordered.lean +++ b/mathlib4/Mathlib/LinearAlgebra/AffineSpace/Ordered.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.CharP.Invertible public import Mathlib.Algebra.Order.Module.Synonym public import Mathlib.LinearAlgebra.AffineSpace.Midpoint public import Mathlib.LinearAlgebra.AffineSpace.Slope +meta import Lean.PostprocessTraces /-! # Ordered modules as affine spaces @@ -28,6 +29,8 @@ for an ordered module interpreted as an affine space. affine space, ordered module, slope -/ +set_option backward.isDefEq.instanceTypes "mark" + public section @@ -95,15 +98,84 @@ set_option backward.isDefEq.respectTransparency false in theorem left_lt_lineMap_iff_lt (h : 0 < r) : a < lineMap a b r ↔ a < b := Iff.trans (by rw [lineMap_apply_zero]) (lineMap_lt_lineMap_iff_of_lt h) +/-! # Issue -/ + set_option backward.isDefEq.respectTransparency false in +set_option backward.isDefEq.instanceTypes "markOrSynth" in theorem lineMap_lt_left_iff_lt (h : 0 < r) : lineMap a b r < a ↔ b < a := left_lt_lineMap_iff_lt (E := Eᵒᵈ) h +/-! ## Explanation -/ + +open Lean.PostprocessTraces + +set_option linter.style.longLine false +-- The `(E := Eᵒᵈ)` transport assigns the goal's `Module k E` data to the lemma's `Eᵒᵈ`-typed +-- binder mvars at default transparency, then synthesizes the leftover `PosSMulReflectLT k Eᵒᵈ` by +-- type. Its `OrderDual.instPosSMulReflectLT` candidate leaves an instance-typed `SMul k E` mvar +-- that has to swallow the goal's `SMul k Eᵒᵈ`-typed slot; the direct `.instances` check fails +-- (`OrderDual` is opaque there). `"mark"` would reject and synthesis would fail — `"markOrSynth"` +-- re-synthesizes `SMul k E` and unifies, rescuing the site. (A fresh `#synth PosSMulReflectLT k Eᵒᵈ` +-- succeeds; only the transport-baked goal is poisoned.) +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +set_option linter.style.longLine false in +/-- +trace: [Meta.synthInstance] ✅️ PosSMulReflectLT k Eᵒᵈ + [Meta.synthInstance.apply] ✅️ apply @OrderDual.instPosSMulReflectLT to PosSMulReflectLT k Eᵒᵈ + [Meta.synthInstance.tryResolve] ✅️ PosSMulReflectLT k Eᵒᵈ ≟ PosSMulReflectLT k Eᵒᵈ + [Meta.isDefEq] ✅️ [instances] PosSMulReflectLT k Eᵒᵈ =?= PosSMulReflectLT ?m.47 ?m.48ᵒᵈ + [Meta.isDefEq] ✅️ [default] DistribMulAction.toDistribSMul.toSMul =?= OrderDual.instSMul + [Meta.isDefEq] ✅️ [default] DistribMulAction.toDistribSMul.toSMul =?= ?m.51 + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.51 : SMul k + E) := (DistribMulAction.toDistribSMul.toSMul : SMul k Eᵒᵈ) + [Meta.isDefEq] ❌️ [instances] SMul k E =?= SMul k Eᵒᵈ + [Meta.isDefEq] ✅️ [instances] k =?= k + [Meta.isDefEq] ❌️ [instances] E =?= Eᵒᵈ + [Meta.isDefEq.onFailure] ❌️ E =?= Eᵒᵈ + [Meta.isDefEq.onFailure] ❌️ SMul k E =?= SMul k Eᵒᵈ + [Meta.synthInstance] ✅️ SMul k E (truncated) + [Meta.isDefEq] ✅️ [default] DistribMulAction.toDistribSMul.toSMul =?= DistribMulAction.toDistribSMul.toSMul (truncated) +--- +warning: Setting options starting with 'debug', 'pp', 'profiler', 'trace' is only intended for development and not for final code. If you intend to submit this contribution to the Mathlib project, please remove 'set_option trace.Meta.synthInstance'. + +Note: This linter can be disabled with `set_option linter.style.setOption false` +-/ +#guard_msgs in +postprocess_traces + filterSubtrees (fun x => (ofClass `Meta.isDefEq.assign.checkTypes x) + <&&> (containsString "toDistribSMul.toSMul :" x)) + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> succeeded x + <&&> containsString "SMul k E" x) + >=> elideBelow (fun x => (ofClass `Meta.isDefEq x) <&&> succeeded x + <&&> containsString "toSMul =?= DistribMulAction" x) +in +set_option backward.isDefEq.respectTransparency false in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +example (h : 0 < r) : lineMap a b r < a ↔ b < a := by + set_option trace.Meta.synthInstance true in + set_option trace.Meta.isDefEq true in + set_option trace.Meta.isDefEq.printTransparency true in + set_option trace.Meta.isDefEq.assign.checkTypes true in + exact left_lt_lineMap_iff_lt (E := Eᵒᵈ) h + set_option backward.isDefEq.respectTransparency false in theorem lineMap_lt_right_iff_lt (h : r < 1) : lineMap a b r < b ↔ a < b := Iff.trans (by rw [lineMap_apply_one]) (lineMap_lt_lineMap_iff_of_lt h) +-- Same `OrderDual` transport as `lineMap_lt_left_iff_lt`; see the Explanation above. set_option backward.isDefEq.respectTransparency false in +set_option backward.isDefEq.instanceTypes "markOrSynth" in theorem right_lt_lineMap_iff_lt (h : r < 1) : b < lineMap a b r ↔ b < a := lineMap_lt_right_iff_lt (E := Eᵒᵈ) h diff --git a/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean b/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean index 36f51dded..a5c3f88b2 100644 --- a/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean +++ b/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean @@ -47,6 +47,11 @@ noncomputable def equivPiTensorComplSingletonTensor (i₀ : ι) : variable (i₀ : ι) +/-! +# Issue (Low Severity) +-/ + +set_option backward.isDefEq.instanceTypes "none" in set_option backward.isDefEq.respectTransparency false in @[simp] lemma equivPiTensorComplSingletonTensor_tprod (i₀ : ι) (m : ∀ i, M i) : @@ -60,6 +65,32 @@ lemma equivPiTensorComplSingletonTensor_tprod (i₀ : ι) (m : ∀ i, M i) : (fun i ↦ M ((Equiv.subtypeNeSumPUnit.{0} i₀) i))] exact (LinearEquiv.lTensor_tmul _ _ _ _).trans (by congr; simp) +/-! +# Fix + +Again the `respectTransparency` interaction. Getting rid of that would help. +-/ +attribute [local implicit_reducible] + Equiv.trans + Equiv.optionSubtype + Equiv.optionEquivSumPUnit + Equiv.refl + Set.singleton + Option.casesOn' + Equiv.optionSubtypeNe + Sum.elim +in +example (i₀ : ι) (m : ∀ i, M i) : + equivPiTensorComplSingletonTensor R M i₀ (⨂ₜ[R] i, m i) = + (⨂ₜ[R] (j : ((Set.singleton i₀)ᶜ : Set ι)), m j) ⊗ₜ m i₀:= by + dsimp [equivPiTensorComplSingletonTensor] + have : (reindex R M (Equiv.subtypeNeSumPUnit.{0} i₀).symm) (⨂ₜ[R] (i : ι), m i) = + ⨂ₜ[R] j, m ((Equiv.subtypeNeSumPUnit.{0} i₀) j) := by + simp_rw [reindex_tprod (R := R) (s := M), Equiv.symm_symm] + rw [dsimp% this, dsimp% tmulEquivDep_symm_apply R + (fun i ↦ M ((Equiv.subtypeNeSumPUnit.{0} i₀) i))] + exact (LinearEquiv.lTensor_tmul _ _ _ _).trans (by congr; simp) + set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma equivPiTensorComplSingletonTensor_symm_tmul (i₀ : ι) diff --git a/mathlib4/Mathlib/ModelTheory/Types.lean b/mathlib4/Mathlib/ModelTheory/Types.lean index 8f9efd01e..9fb791833 100644 --- a/mathlib4/Mathlib/ModelTheory/Types.lean +++ b/mathlib4/Mathlib/ModelTheory/Types.lean @@ -41,7 +41,6 @@ This file defines the space of complete types over a first-order theory. @[expose] public section - universe u v w w' open Cardinal Set FirstOrder @@ -237,6 +236,11 @@ def realizedTypes (α : Type w) : Set (T.CompleteType α) := section +/-! +# Issue (Mid Severity) +-/ + +set_option backward.isDefEq.instanceTypes "none" in set_option backward.isDefEq.respectTransparency false in theorem exists_modelType_is_realized_in (p : T.CompleteType α) : ∃ M : Theory.ModelType.{u, v, max u v w} T, p ∈ T.realizedTypes M α := by @@ -251,6 +255,29 @@ theorem exists_modelType_is_realized_in (p : T.CompleteType α) : (p.isMaximal.mem_iff_models φ).symm) rfl +/-! +# Fix + +Add `implicit_reducible` attributes, and `cast` the `M.struct` instance to the correct expected +type. + +`cast rfl` is a quick and dirty fix. It would be better to find a more sustainable solution. +-/ + +attribute [local implicit_reducible] ModelType.reduct ModelType.subtheoryModel in +example (p : T.CompleteType α) : + ∃ M : Theory.ModelType.{u, v, max u v w} T, p ∈ T.realizedTypes M α := by + obtain ⟨M⟩ := p.isMaximal.1 + refine ⟨(M.subtheoryModel p.subset).reduct (L.lhomWithConstants α), fun a => (L.con a : M), ?_⟩ + refine SetLike.ext fun φ => ?_ + simp only [CompleteType.mem_typeOf] + refine + (@Formula.realize_equivSentence_symm_con _ + ((M.subtheoryModel p.subset).reduct (L.lhomWithConstants α)) _ _ (cast rfl M.struc) _ φ).trans + (_root_.trans (_root_.trans ?_ (p.isMaximal.isComplete.realize_sentence_iff φ M)) + (p.isMaximal.mem_iff_models φ).symm) + rfl + end end Theory diff --git a/mathlib4/Mathlib/NumberTheory/Padics/WithVal.lean b/mathlib4/Mathlib/NumberTheory/Padics/WithVal.lean index 641d6ab71..e61b71cfa 100644 --- a/mathlib4/Mathlib/NumberTheory/Padics/WithVal.lean +++ b/mathlib4/Mathlib/NumberTheory/Padics/WithVal.lean @@ -35,7 +35,12 @@ variable {p : ℕ} [Fact p.Prime] open NNReal WithZero UniformSpace +/-! +# Issue (Low Severity) +-/ + set_option backward.isDefEq.respectTransparency.types false in +set_option backward.isDefEq.instanceTypes "none" in open MonoidWithZeroHom.ValueGroup₀ in lemma isUniformInducing_cast_withVal : IsUniformInducing ((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) := by @@ -90,6 +95,75 @@ lemma isUniformInducing_cast_withVal : IsUniformInducing ((Rat.castHom ℚ_[p]). Int.lt_iff_add_one_le] · simp [Nat.Prime.ne_zero Fact.out] +/-! +# Fix + +Get rid of `respectTransparency`. +-/ + +attribute [local implicit_reducible] + Rat.padicValuation + Valuation.restrict + coe + exp + Multiplicative.ofAdd + Additive.ofMul + Multiplicative.toAdd +in +open MonoidWithZeroHom.ValueGroup₀ in +example : IsUniformInducing ((Rat.castHom ℚ_[p]).comp + (WithVal.equiv (Rat.padicValuation p)).toRingHom) := by + have hp0' : 0 < (p : ℚ) := by simp [Nat.Prime.pos Fact.out] + have hp0 : 0 < (p : ℝ)⁻¹ := by simp [Nat.Prime.pos Fact.out] + have hp1' : 1 < (p : ℚ) := by simp [Nat.Prime.one_lt Fact.out] + have hp1 : (p : ℝ)⁻¹ < 1 := by simp [inv_lt_one_iff₀, Nat.Prime.one_lt Fact.out] + rw [Filter.HasBasis.isUniformInducing_iff (Valued.hasBasis_uniformity _ _) + (Metric.uniformity_basis_dist_le_pow hp0 hp1)] + simp only [Set.mem_ofPred_eq, dist_eq_norm_sub, inv_pow, RingEquiv.toRingHom_eq_coe, + RingHom.coe_comp, Rat.coe_castHom, RingHom.coe_coe, Function.comp_apply, ← Rat.cast_sub, + ← map_sub, Padic.eq_padicNorm, true_and, forall_const] + constructor + · intro n + have hn : Valued.v (R := (WithVal (Rat.padicValuation p))) (p ^ n) = + exp (-n : ℤ) := by + simp only [← WithVal.val_apply_equiv, map_pow, map_natCast, Rat.padicValuation_self, + Int.reduceNeg, exp_neg, inv_pow, ← exp_nsmul, nsmul_eq_mul, mul_one] + use Units.mk0 (Valued.v.restrict (p ^ n)) (by + simp [Valuation.restrict_def, Nat.Prime.ne_zero Fact.out]) + intro x y h + set x' := (WithVal.equiv (Rat.padicValuation p)) x with hx + set y' := (WithVal.equiv (Rat.padicValuation p)) y with hy + rw [Valuation.map_sub_swap, Units.val_mk0, Valuation.restrict_lt_iff, hn] at h + change Rat.padicValuation p (x' - y') < exp _ at h + rw [← Nat.cast_pow, ← Rat.cast_natCast, ← Rat.cast_inv_of_ne_zero, Rat.cast_le] + · rw [map_sub, ← hx, ← hy] + simp only [Rat.padicValuation, Valuation.coe_mk, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, + padicNorm, zpow_neg, Nat.cast_pow] at h ⊢ + split_ifs with H + · simp + · simp only [H, ↓reduceIte, exp_lt_exp, neg_lt_neg_iff] at h + simpa [hp0', zpow_pos, pow_pos, inv_le_inv₀] using + zpow_right_mono₀ (by exact_mod_cast (Nat.Prime.one_le Fact.out)) h.le + · simp [Nat.Prime.ne_zero Fact.out] + · intro γ + use (log ((embedding γ.val) * exp (-1))).natAbs + intro x y h + set x' := (WithVal.equiv (Rat.padicValuation p)) x with hx + set y' := (WithVal.equiv (Rat.padicValuation p)) y with hy + rw [Valuation.map_sub_swap, Valuation.restrict_lt_iff_lt_embedding] + change Rat.padicValuation p (x' - y') < embedding γ.1 + rw [← Nat.cast_pow, ← Rat.cast_natCast, ← Rat.cast_inv_of_ne_zero, Rat.cast_le] at h + · change padicNorm p (x' - y') ≤ _ at h + simp only [Rat.padicValuation, Valuation.coe_mk, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, + padicNorm, zpow_neg, Nat.cast_pow] at h ⊢ + split_ifs with H + · simp only [exp_neg] + exact embedding_unit_pos _ + · rw [← lt_log_iff_exp_lt (embedding_unit_ne_zero _)] + simp_all [← zpow_natCast, zpow_pos, inv_le_inv₀, zpow_le_zpow_iff_right₀ hp1', abs_le, + Int.lt_iff_add_one_le] + · simp [Nat.Prime.ne_zero Fact.out] + lemma isDenseInducing_cast_withVal : IsDenseInducing ((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) := by refine Padic.isUniformInducing_cast_withVal.isDenseInducing ?_ diff --git a/mathlib4/Mathlib/Order/Hom/Bounded.lean b/mathlib4/Mathlib/Order/Hom/Bounded.lean index 95142ff2e..fb642edf7 100644 --- a/mathlib4/Mathlib/Order/Hom/Bounded.lean +++ b/mathlib4/Mathlib/Order/Hom/Bounded.lean @@ -431,6 +431,8 @@ theorem coe_comp_orderHom (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β (f.comp g : OrderHom α γ) = (f : OrderHom β γ).comp g := rfl +-- TODO: This fails +-- set_option backward.isDefEq.instanceTypes "markOrSynthOrStuck" in @[to_dual (attr := simp)] theorem coe_comp_topHom (f : BoundedOrderHom β γ) (g : BoundedOrderHom α β) : (f.comp g : TopHom α γ) = (f : TopHom β γ).comp g := diff --git a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean index 5fda00c63..491e2cfbb 100644 --- a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean +++ b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean @@ -114,7 +114,6 @@ theorem range_d₁₀_eq_coinvariantsKer : simpa [← hy, add_sub_add_comm, sum_add_index, d₁₀_single (G := G)] using! Submodule.add_mem _ (Coinvariants.mem_ker_of_eq _ _ _ rfl) (h rfl) -set_option backward.isDefEq.respectTransparency false in set_option backward.defeqAttrib.useBackward true in @[reassoc (attr := simp), elementwise (attr := simp)] lemma d₁₀_comp_coinvariantsMk : d₁₀ A ≫ (coinvariantsMk k G).app A = 0 := by diff --git a/mathlib4/Mathlib/RepresentationTheory/Induced.lean b/mathlib4/Mathlib/RepresentationTheory/Induced.lean index 2677fd901..7b892ac5a 100644 --- a/mathlib4/Mathlib/RepresentationTheory/Induced.lean +++ b/mathlib4/Mathlib/RepresentationTheory/Induced.lean @@ -179,7 +179,6 @@ variable {G H : Type u} [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : R open Representation set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear map `(Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G` sending `⟦h ⊗ₜ a⟧ ⊗ₜ b` to `⟦a ⊗ ρ(h)(b)⟧` for all `h : H`, `a : A`, and `b : B`. -/ @@ -198,7 +197,6 @@ noncomputable def coinvariantsTensorIndHom : ext; simp set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in variable {A B} in lemma coinvariantsTensorIndHom_mk_tmul_indVMk (h : H) (x : A) (y : B) : coinvariantsTensorIndHom φ A B (coinvariantsTensorMk _ _ (IndV.mk φ _ h x) y) = @@ -206,7 +204,6 @@ lemma coinvariantsTensorIndHom_mk_tmul_indVMk (h : H) (x : A) (y : B) : simp [coinvariantsTensorIndHom, coinvariantsTensorMk] set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear map `(A ⊗ Res(φ)(B))_G ⟶ (Ind(φ)(A) ⊗ B))_H` sending `⟦a ⊗ₜ b⟧` to `⟦1 ⊗ₜ a⟧ ⊗ₜ b` for all `a : A`, and `b : B`. -/ @@ -223,7 +220,6 @@ noncomputable def coinvariantsTensorIndInv : simp [← Coinvariants.mk_inv_tmul] set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in variable {A B} in lemma coinvariantsTensorIndInv_mk_tmul_indMk (x : A) (y : B) : coinvariantsTensorIndInv φ A B (Coinvariants.mk @@ -232,7 +228,6 @@ lemma coinvariantsTensorIndInv_mk_tmul_indMk (x : A) (y : B) : simp [coinvariantsTensorIndInv, coinvariantsTensorMk] set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear isomorphism `(Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G` sending `⟦h ⊗ₜ a⟧ ⊗ₜ b` to `⟦a ⊗ ρ(h)(b)⟧` for all `h : H`, `a : A`, and `b : B`. -/ @@ -252,7 +247,6 @@ noncomputable def coinvariantsTensorIndIso : simp [coinvariantsTensorIndInv, coinvariantsTensorMk, coinvariantsTensorIndHom] set_option backward.defeqAttrib.useBackward true in -set_option backward.isDefEq.respectTransparency false in /-- Given a group hom `φ : G →* H` and `A : Rep k G`, the functor `Rep k H ⥤ ModuleCat k` sending `B ↦ (Ind(φ)(A) ⊗ B))_H` is naturally isomorphic to the one sending `B ↦ (A ⊗ Res(φ)(B))_G`. -/ @[simps! hom_app inv_app] diff --git a/mathlib4/Mathlib/RepresentationTheory/Intertwining.lean b/mathlib4/Mathlib/RepresentationTheory/Intertwining.lean index 428ad6f57..168bb25fc 100644 --- a/mathlib4/Mathlib/RepresentationTheory/Intertwining.lean +++ b/mathlib4/Mathlib/RepresentationTheory/Intertwining.lean @@ -6,6 +6,7 @@ Authors: Stepan Nesterov, Edison Xie module public import Mathlib.RepresentationTheory.Subrepresentation +meta import Lean.PostprocessTraces /-! # Intertwining maps @@ -14,6 +15,8 @@ This file gives defines intertwining maps of representations (aka equivariant li -/ +set_option backward.isDefEq.instanceTypes "mark" + @[expose] public section open scoped MonoidAlgebra @@ -486,6 +489,27 @@ instance : Module A (IntertwiningMap ρ σ) := fast_instance% Function.Injective.module A (coeFnAddMonoidHom ρ σ) DFunLike.coe_injective (coe_smul ρ σ) +open Lean.PostprocessTraces + +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +/-! # Issue (Low Severity) -/ + +/- +If `asModule` is made implicit-reducible *at its definition site*, then `respectTransparency` false +becomes obsolete. After removing it, the lemma also works with "markOrSynth". +-/ +set_option backward.isDefEq.instanceTypes "none" in set_option backward.isDefEq.respectTransparency false in /-- An intertwining map is the same thing as a linear map over the group ring. -/ def equivLinearMapAsModule : @@ -507,6 +531,123 @@ def equivLinearMapAsModule : left_inv f := rfl right_inv f := rfl +/-! +# Explanation + +Bad interaction with `respectTransparency false`, which disables the implicit bump. +Therefore, the synthesized and unified values are compared at ambient, instances, transparency, +and the comparison fails. It would succeed if there was an implicit bump and `asModule` was +implicit-reducible. +Data point in favor for packaging all the backward compatibility flags. +-/ +set_option linter.style.longLine false in +/-- +error: `simp` made no progress + +Note: The target expression is not type-correct under the `implicit` transparency level, which may have triggered the failure. This is usually caused by unfolding of semireducible definitions in prior tactic steps. Use `set_option linter.tacticCheckInstances true` to investigate the source of the issue. +Full error: + Application type mismatch: The argument + a • v + has type + V + but is expected to have type + ρ.asModule + in the application + f (a • v) +--- +trace: [Meta.isDefEq] ✅️ [reducible] ?f (?c • ?x) =?= f (a • v) + [Meta.isDefEq] ✅️ [reducible] ?c • ?x =?= a • v + [Meta.isDefEq] ✅️ [default] instHSMul =?= instHSMul + [Meta.isDefEq] ✅️ [default] ?inst✝ =?= DistribMulAction.toDistribSMul.toSMul + [Meta.isDefEq.assign.checkTypes] ✅️ (?inst✝ : SMul A + ρ.asModule) := (DistribMulAction.toDistribSMul.toSMul : SMul A V) + [Meta.isDefEq] ✅️ [default] SMul A ρ.asModule =?= SMul A V + [Meta.isDefEq] ✅️ [default] A =?= A + [Meta.isDefEq] ✅️ [default] ρ.asModule =?= V +[Meta.synthInstance] ✅️ SMul A σ.asModule + [Meta.isDefEq] ✅️ [instances] ?m.83 =?= DistribMulAction.toDistribSMul + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.83 : DistribSMul A + σ.asModule) := (DistribMulAction.toDistribSMul : DistribSMul A σ.asModule) + [Meta.isDefEq] ✅️ [instances] DistribSMul A σ.asModule =?= DistribSMul A σ.asModule + [Meta.isDefEq] ✅️ [instances] A =?= A + [Meta.isDefEq] ✅️ [instances] σ.asModule =?= σ.asModule + [Meta.isDefEq] ✅️ [default] σ.instAddCommMonoidAsModule.toAddZeroClass =?= σ.instAddCommMonoidAsModule.toAddZeroClass +[Meta.isDefEq] ✅️ [instances] ?inst✝ =?= DistribMulAction.toDistribSMul.toSMul + [Meta.isDefEq.assign.checkTypes] ✅️ (?inst✝ : SMul A + σ.asModule) := (DistribMulAction.toDistribSMul.toSMul : SMul A σ.asModule) + [Meta.isDefEq] ✅️ [default] SMul A σ.asModule =?= SMul A σ.asModule + [Meta.isDefEq] ✅️ [default] A =?= A + [Meta.isDefEq] ✅️ [default] σ.asModule =?= σ.asModule +[Meta.isDefEq] ✅️ [reducible] ?fₗ (?c • ?x) =?= f (a • v) + [Meta.isDefEq] ✅️ [reducible] ?c • ?x =?= a • v + [Meta.isDefEq] ✅️ [default] instHSMul =?= instHSMul + [Meta.isDefEq] ✅️ [default] ?inst✝ =?= DistribMulAction.toDistribSMul.toSMul + [Meta.isDefEq.assign.checkTypes] ✅️ (?inst✝ : SMul A + ρ.asModule) := (DistribMulAction.toDistribSMul.toSMul : SMul A V) + [Meta.isDefEq] ✅️ [default] SMul A ρ.asModule =?= SMul A V + [Meta.isDefEq] ✅️ [default] A =?= A + [Meta.isDefEq] ✅️ [default] ρ.asModule =?= V +[Meta.isDefEq] ✅️ [instances] ?inst✝ =?= DistribMulAction.toDistribSMul.toSMul + [Meta.isDefEq.assign.checkTypes] ✅️ (?inst✝ : SMul A + σ.asModule) := (DistribMulAction.toDistribSMul.toSMul : SMul A σ.asModule) + [Meta.isDefEq] ✅️ [default] SMul A σ.asModule =?= SMul A σ.asModule + [Meta.isDefEq] ✅️ [default] A =?= A + [Meta.isDefEq] ✅️ [default] σ.asModule =?= σ.asModule +[Meta.synthInstance] ❌️ LinearMap.CompatibleSMul ρ.asModule σ.asModule A A[G] + [Meta.synthInstance.apply] ❌️ apply @LinearMap.IsScalarTower.compatibleSMul to LinearMap.CompatibleSMul ρ.asModule + σ.asModule A A[G] + [Meta.synthInstance.tryResolve] ❌️ LinearMap.CompatibleSMul ρ.asModule σ.asModule A + A[G] ≟ LinearMap.CompatibleSMul ?m.80 ?m.81 ?m.84 ?m.85 + [Meta.isDefEq] ❌️ [instances] LinearMap.CompatibleSMul ρ.asModule σ.asModule A + A[G] =?= LinearMap.CompatibleSMul ?m.80 ?m.81 ?m.84 ?m.85 + [Meta.isDefEq] ❌️ [instances] DistribMulAction.toDistribSMul.toSMul =?= ?m.87 + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.87 : SMul A + ρ.asModule) := (DistribMulAction.toDistribSMul.toSMul : SMul A V) + [Meta.isDefEq] ❌️ [instances] SMul A ρ.asModule =?= SMul A V + [Meta.isDefEq] ✅️ [instances] A =?= A + [Meta.isDefEq] ❌️ [instances] ρ.asModule =?= V + [Meta.isDefEq.onFailure] ❌️ ρ.asModule =?= V + [Meta.isDefEq.onFailure] ❌️ SMul A ρ.asModule =?= SMul A V + [Meta.synthInstance] ✅️ SMul A ρ.asModule (truncated) + [Meta.isDefEq] ❌️ [instances] DistribMulAction.toDistribSMul.toSMul =?= DistribMulAction.toDistribSMul.toSMul + [Meta.isDefEq] ❌️ [instances] DistribMulAction.toDistribSMul.toSMulZeroClass.1 =?= DistribMulAction.toDistribSMul.toSMulZeroClass.1 + [Meta.isDefEq] ❌️ [instances] inst✝².toSMul =?= ρ.instModuleAsModule.toSMul + [Meta.isDefEq] ❌️ [instances] inst✝².toSemigroupAction.1 =?= ρ.instModuleAsModule.toSemigroupAction.1 + [Meta.isDefEq] ❌️ [instances] inst✝².toSemigroupAction.1 =?= instModuleAsModule._aux_1 ρ + [Meta.isDefEq.onFailure] ❌️ inst✝².toSemigroupAction.1 =?= instModuleAsModule._aux_1 ρ + [Meta.isDefEq.assign.checkTypes] ❌️ (?m.87 : SMul A ρ.asModule) := (inst✝².toSemigroupAction.1 : SMul A V) + [Meta.isDefEq] ❌️ [instances] SMul A ρ.asModule =?= SMul A V + [Meta.isDefEq] ✅️ [instances] A =?= A + [Meta.isDefEq] ❌️ [instances] ρ.asModule =?= V + [Meta.isDefEq.onFailure] ❌️ ρ.asModule =?= V + [Meta.isDefEq.onFailure] ❌️ SMul A ρ.asModule =?= SMul A V + [Meta.synthInstance] ✅️ SMul A ρ.asModule (truncated) + [Meta.isDefEq] ❌️ [instances] inst✝².toSemigroupAction.1 =?= DistribMulAction.toDistribSMul.toSMul + [Meta.isDefEq] ❌️ [instances] inst✝².toSemigroupAction.1 =?= DistribMulAction.toDistribSMul.toSMulZeroClass.1 + [Meta.isDefEq] ❌️ [instances] inst✝².toSemigroupAction.1 =?= ρ.instModuleAsModule.toSMul + [Meta.isDefEq] ❌️ [instances] inst✝².toSemigroupAction.1 =?= ρ.instModuleAsModule.toSemigroupAction.1 + [Meta.isDefEq] ❌️ [instances] inst✝².toSemigroupAction.1 =?= instModuleAsModule._aux_1 ρ + [Meta.isDefEq.onFailure] ❌️ inst✝².toSemigroupAction.1 =?= instModuleAsModule._aux_1 ρ +-/ +#guard_msgs in +postprocess_traces + filterSubtrees (fun x => + ((ofClass `Meta.synthInstance.apply x) <&&> (containsString "compatibleSMul" x)) <||> + ((ofClass `Meta.isDefEq.assign.checkTypes x) + <&&> (containsString "SMul A" x) <&&> (containsString "asModule" x))) + >=> filterSubtrees (fun x => (ofClass `Meta.isDefEq.assign.checkTypes x) + <&&> (containsString "SMul A" x)) + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) <&&> (containsString "SMul A ρ.asModule" x)) +in +set_option backward.isDefEq.respectTransparency false in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +example (f : ρ.asModule →ₗ[A[G]] σ.asModule) (a : A) (v : V) : f (a • v) = a • f v := by + set_option trace.Meta.synthInstance true in + set_option trace.Meta.isDefEq.assign.checkTypes true in + set_option trace.Meta.isDefEq true in + set_option trace.Meta.isDefEq.printTransparency true in + simp + set_option backward.isDefEq.respectTransparency false in /-- Composition of intertwining maps. -/ def llcomp : IntertwiningMap σ τ →ₗ[A] IntertwiningMap ρ σ →ₗ[A] IntertwiningMap ρ τ where diff --git a/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basis.lean b/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basis.lean index 6a4cc4ce7..4220606ae 100644 --- a/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basis.lean +++ b/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basis.lean @@ -236,22 +236,47 @@ set_option backward.isDefEq.respectTransparency false in def basisRight : Module.Basis Unit S D.presRight.toExtension.Cotangent := Generators.basisCotangentAway S D.gbar +/-! +# Issue (Low Severity) + +Uncontroversial fix, shared by the three `instanceTypes "none"` sites in this file. +Making `Algebra.Generators.toExtension` implicit-reducible obsoletes both +`respectTransparency(.types) false` and `instanceTypes "none"`. +-/ + set_option backward.isDefEq.respectTransparency.types false in +set_option backward.isDefEq.instanceTypes "none" in /-- The basis on the cotangent space of the constructed presentation. -/ def basis [Nontrivial S] : Module.Basis (Unit ⊕ σ) S D.pres.toExtension.Cotangent := (Module.Basis.prod D.basisRight D.basisLeft).map D.cotangentEquivProd.symm +/-! # Fix -/ + +attribute [local implicit_reducible] toExtension in +example [Nontrivial S] : Module.Basis (Unit ⊕ σ) S D.pres.toExtension.Cotangent := + (Module.Basis.prod D.basisRight D.basisLeft).map D.cotangentEquivProd.symm + set_option backward.isDefEq.respectTransparency false in lemma basis_inl [Nontrivial S] : D.basis (.inl ()) = D.cotangentEquivProd.symm (Generators.cMulXSubOneCotangent S D.gbar, 0) := by simpa [basis] using! Generators.basisCotangentAway_apply _ _ +/-! # Issue 2 (Low Severity, same fix) -/ + set_option backward.isDefEq.respectTransparency.types false in +set_option backward.isDefEq.instanceTypes "none" in lemma basis_inr [Nontrivial S] (i : σ) : D.basis (.inr i) = D.cotangentEquivProd.symm (0, D.basisLeft i) := by simp [basis] +/-! # Fix -/ + +attribute [local implicit_reducible] toExtension in +example [Nontrivial S] (i : σ) : + D.basis (.inr i) = D.cotangentEquivProd.symm (0, D.basisLeft i) := by + simp [basis] + lemma pres_val_comp_inr : D.pres.val ∘ Sum.inr = P.val := funext (aeval_X _) set_option backward.isDefEq.respectTransparency false in @@ -273,6 +298,15 @@ end PresentationOfFreeCotangent.Aux end +/-! +# Issue 3 (Low Severity, same fix) + +`attribute [local implicit_reducible] Algebra.Generators.toExtension` also lets both +`respectTransparency false` and `instanceTypes "none"` go here; no `example` since the +proof is long. +-/ + +set_option backward.isDefEq.instanceTypes "none" in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in open PresentationOfFreeCotangent in diff --git a/mathlib4/Mathlib/RingTheory/Kaehler/Basic.lean b/mathlib4/Mathlib/RingTheory/Kaehler/Basic.lean index 828517e10..a573eed3b 100644 --- a/mathlib4/Mathlib/RingTheory/Kaehler/Basic.lean +++ b/mathlib4/Mathlib/RingTheory/Kaehler/Basic.lean @@ -192,6 +192,13 @@ theorem KaehlerDifferential.DLinearMap_apply (s : S) : (KaehlerDifferential.ideal R S).toCotangent ⟨1 ⊗ₜ s - s ⊗ₜ 1, KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R s⟩ := rfl +/-! +# Issue (Low Severity) + +Fixed by making `KaehlerDifferential` implicit-reducible at definition site. +-/ + +set_option backward.isDefEq.instanceTypes "none" in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The universal derivation into `Ω[S⁄R]`. -/ diff --git a/mathlib4/Mathlib/RingTheory/Kaehler/JacobiZariski.lean b/mathlib4/Mathlib/RingTheory/Kaehler/JacobiZariski.lean index ee13f7d06..7263855d4 100644 --- a/mathlib4/Mathlib/RingTheory/Kaehler/JacobiZariski.lean +++ b/mathlib4/Mathlib/RingTheory/Kaehler/JacobiZariski.lean @@ -9,6 +9,7 @@ public import Mathlib.RingTheory.Extension.Cotangent.Basic public import Mathlib.RingTheory.Extension.Generators public import Mathlib.Algebra.Module.SnakeLemma public import Mathlib.RingTheory.Flat.Basic +meta import Lean.PostprocessTraces /-! @@ -51,6 +52,8 @@ for `Tor` modules is available. -/ +set_option backward.isDefEq.instanceTypes "mark" + @[expose] public section open KaehlerDifferential Module MvPolynomial TensorProduct @@ -284,6 +287,9 @@ lemma δAux_toAlgHom (f : Hom Q Q') (x) : rw [add_left_comm] rfl +/-! # Issue -/ + +set_option backward.isDefEq.instanceTypes "markOrSynth" in set_option backward.isDefEq.respectTransparency false in lemma δAux_ofComp (x : (Q.comp P).Ring) : δAux R Q ((Q.ofComp P).toAlgHom x) = @@ -316,6 +322,100 @@ lemma δAux_ofComp (x : (Q.comp P).Ring) : toKaehler_cotangentSpaceBasis, add_left_inj, LinearMap.coe_inl] rfl +/-! ## Explanation + +The `mul_X` `simp only` rewrites `1 ⊗ₜ (X n • D p)` with `TensorProduct.tmul_smul`, whose +`[CompatibleSMul …]` hypothesis is synthesized. The only candidate `CompatibleSMul.isScalarTower` +reproduces a `Module _ T` slot in an instance-typed mvar; the direct check then compares +`Module (Q.comp P).Ring T =?= Module (Q.comp P).toExtension.Ring T` at `.instances`, where the +semireducible `Generators.toExtension` does not unfold, so the candidate value (spelled at +`(Q.comp P).toExtension.Ring`) is rejected. Under `"markOrSynth"` the mvar is re-synthesized at its +own type — which returns the same instance — and the following unification succeeds, so `tmul_smul` +fires. Same `Ring`/`toExtension.Ring` boundary as the remaining site in +`Mathlib/RingTheory/Extension/Cotangent/Basis.lean`; the rejected mvar is data-valued (`Module`), +so a Prop-exemption would not apply even though `CompatibleSMul` is a Prop. +-/ + +open Lean.PostprocessTraces + +private meta partial def dropSubtrees (p : TracePattern) : TracePostprocessor := + fun trees => trees.filterMapM go +where + go (t : TraceTree) : Lean.CoreM (Option TraceTree) := do + if ← p t then + return none + match t with + | .leaf msg => return some (.leaf msg) + | .node data msg children wrap => return some (.node data msg (← children.filterMapM go) wrap) + +private meta partial def elideBelow (p : TracePattern) : TracePostprocessor := + fun trees => trees.mapM go +where + go (t : TraceTree) : Lean.CoreM TraceTree := do + match t with + | .leaf msg => return .leaf msg + | .node data msg children wrap => + if ← p t then + return .node data m!"{msg} (truncated)" #[] wrap + else + return .node data msg (← children.mapM go) wrap + +set_option linter.style.longLine false in +/-- +trace: [Meta.synthInstance] ✅️ CompatibleSMul (Q.comp P).Ring (Q.comp P).Ring T Ω[(Q.comp P).Ring⁄R] + [Meta.synthInstance.apply] ✅️ apply @CompatibleSMul.isScalarTower to CompatibleSMul (Q.comp P).Ring (Q.comp P).Ring T + Ω[(Q.comp P).Ring⁄R] + [Meta.synthInstance.tryResolve] ✅️ CompatibleSMul (Q.comp P).Ring (Q.comp P).Ring T + Ω[(Q.comp P).Ring⁄R] ≟ CompatibleSMul (Q.comp P).Ring (Q.comp P).Ring T Ω[(Q.comp P).Ring⁄R] + [Meta.isDefEq] ✅️ [instances] CompatibleSMul (Q.comp P).Ring (Q.comp P).Ring T + Ω[(Q.comp P).Ring⁄R] =?= CompatibleSMul ?m.270 ?m.271 ?m.274 ?m.275 + [Meta.isDefEq] ✅️ [instances] toModule =?= ?m.279 + [Meta.isDefEq.assign.checkTypes] ✅️ (?m.279 : Module (Q.comp P).Ring + T) := (toModule : Module (Q.comp P).toExtension.Ring T) + [Meta.isDefEq] ❌️ [instances] Module (Q.comp P).Ring T =?= Module (Q.comp P).toExtension.Ring T (truncated) + [Meta.synthInstance] ✅️ Module (Q.comp P).Ring T (truncated) + [Meta.isDefEq] ✅️ [instances] toModule =?= toModule +--- +warning: declaration uses `sorry` +-/ +#guard_msgs in +postprocess_traces + filterSubtrees (fun x => (ofClass `Meta.synthInstance.apply x) + <&&> (containsString "CompatibleSMul.isScalarTower" x)) + >=> filterSubtrees (fun x => (ofClass `Meta.isDefEq.assign.checkTypes x) + <&&> (containsString "toExtension.Ring T" x) <&&> succeeded x) + >=> dropSubtrees (ofClass `Meta.isDefEq.onFailure) + >=> elideBelow (fun x => (failed x) <&&> (containsString "toExtension.Ring T" x)) + >=> elideBelow (fun x => (ofClass `Meta.synthInstance x) + <&&> (containsString "Module (Q.comp P).Ring T" x)) + >=> dropSubtrees (fun x => (containsString "[default]" x)) +in +set_option backward.isDefEq.instanceTypes "markOrSynth" in +set_option backward.isDefEq.respectTransparency false in +set_option linter.unusedSimpArgs false in +set_option linter.style.setOption false in +example (x : (Q.comp P).Ring) : + δAux R Q ((Q.ofComp P).toAlgHom x) = + P.toExtension.toKaehler.baseChange T (CotangentSpace.compEquiv Q P + (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) x : _)).2 := by + let : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance + have : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T := IsScalarTower.left _ + induction x using MvPolynomial.induction_on with + | C s => sorry + | add x₁ x₂ hx₁ hx₂ => sorry + | mul_X p n IH => + set_option trace.Meta.synthInstance true in + set_option trace.Meta.isDefEq true in + set_option trace.Meta.isDefEq.printTransparency true in + set_option trace.Meta.isDefEq.assign.checkTypes true in + simp only [map_mul, Hom.toAlgHom_X, ofComp_val, δAux_mul, + ← @IsScalarTower.algebraMap_smul Q.Ring T, algebraMap_apply, Hom.algebraMap_toAlgHom, + algebraMap_self, map_aeval, RingHomCompTriple.comp_eq, comp_val, RingHom.id_apply, + IH, Derivation.leibniz, tmul_add, tmul_smul, ← cotangentSpaceBasis_apply, coe_eval₂Hom, + ← @IsScalarTower.algebraMap_smul (Q.comp P).Ring T, aeval_X, map_smul, Prod.snd_add, + Prod.smul_snd, map_add] + sorry + lemma map_comp_cotangentComplex_baseChange : (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom).liftBaseChange T ∘ₗ P.toExtension.cotangentComplex.baseChange T = diff --git a/mathlib4/Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean b/mathlib4/Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean index a2effb36e..483d06a5a 100644 --- a/mathlib4/Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean +++ b/mathlib4/Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean @@ -13,6 +13,8 @@ public import Mathlib.RingTheory.Polynomial.Resultant.Basic public import Mathlib.RingTheory.Smooth.StandardSmoothCotangent public import Mathlib.RingTheory.LocalRing.ResidueField.Ideal +meta import Lean.PostprocessTraces + /-! @@ -31,6 +33,8 @@ We construct the universal ring of the following functors on `R-Alg`: -/ +open Lean.PostprocessTraces + @[expose] public section open scoped Polynomial TensorProduct @@ -187,11 +191,17 @@ def universalFactorizationMapLiftEquiv (p : MonicDegreeEq S n) : left_inv f := by ext <;> simp right_inv q := by ext <;> simp -set_option backward.isDefEq.respectTransparency.types false in +/-! +# Issue + +Fixed after adjusting the `onFailure` logic in `isDefEqApp`. +-/ + lemma ker_eval₂Hom_universalFactorizationMap : RingHom.ker (eval₂Hom (S₁ := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) (universalFactorizationMap R n m k hn) (Sum.elim (.X · ⊗ₜ 1) (1 ⊗ₜ .X ·))) = - Ideal.span (Set.range fun i ↦ C (X i) - map C (tensorEquivSum _ _ _ _ + Ideal.span (Set.range fun i ↦ C (X i) - + map C (tensorEquivSum _ _ _ _ (universalFactorizationMap R n m k hn (X i)))) := by set f := eval₂Hom (R := MvPolynomial (Fin n) R) (S₁ := MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) @@ -221,6 +231,9 @@ lemma ker_eval₂Hom_universalFactorizationMap : congr 1 ext <;> simp +postprocess_traces + filterSubtrees fun x => containsString "=?= Mul.mul" x +in set_option backward.isDefEq.respectTransparency false in /-- The canonical presentation of `universalFactorizationMap`. -/ @[simps] def universalFactorizationMapPresentation : @@ -514,7 +527,12 @@ def UniversalFactorizationRing.presentation : letI := ((MvPolynomial.mapEquivMonic R _ n).symm p).toAlgebra (MvPolynomial.universalFactorizationMapPresentation R n m k hn).baseChange _ -set_option backward.isDefEq.respectTransparency.types false in +/-! +# Issue 2 (Low Severity) + +Same. +-/ + lemma UniversalFactorizationRing.jacobian_resentation : (presentation m k hn p).jacobian = (-1) ^ n * (factor₁ m k hn p).1.resultant (factor₂ m k hn p).1 := by diff --git a/mathlib4/Mathlib/RingTheory/Regular/RegularSequence.lean b/mathlib4/Mathlib/RingTheory/Regular/RegularSequence.lean index 9b58c8f23..62eeffd2f 100644 --- a/mathlib4/Mathlib/RingTheory/Regular/RegularSequence.lean +++ b/mathlib4/Mathlib/RingTheory/Regular/RegularSequence.lean @@ -571,7 +571,12 @@ lemma map_first_exact_on_four_term_right_exact_of_isSMulRegular_last section Perm +/-! +# Issue (Low Severity) +-/ + set_option backward.isDefEq.respectTransparency.types false in +set_option backward.isDefEq.instanceTypes "none" in open _root_.LinearMap in private lemma IsWeaklyRegular.swap {a b : R} (h1 : IsWeaklyRegular M [a, b]) (h2 : torsionBy R M b = a • torsionBy R M b → torsionBy R M b = ⊥) : @@ -587,6 +592,31 @@ private lemma IsWeaklyRegular.swap {a b : R} (h1 : IsWeaklyRegular M [a, b]) · rwa [ha.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, inf_comm, smul_comm, ← h2.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, and_iff_left hb] +/-! +# Fix + +add implicit reducibility attributes? +-/ + +attribute [local implicit_reducible] + torsionBy DistribSMul.toLinearMap + LinearMap.lsmul LinearMap.mk₂ LinearMap.mk₂' LinearMap.mk₂'ₛₗ +in +open _root_.LinearMap in +example {a b : R} (h1 : IsWeaklyRegular M [a, b]) + (h2 : torsionBy R M b = a • torsionBy R M b → torsionBy R M b = ⊥) : + IsWeaklyRegular M [b, a] := by + rw [isWeaklyRegular_cons_iff, isWeaklyRegular_singleton_iff] at h1 ⊢ + obtain ⟨ha, hb⟩ := h1 + rw [← isSMulRegular_iff_torsionBy_eq_bot] at h2 + specialize h2 (le_antisymm ?_ (smul_le_self_of_tower a (torsionBy R M b))) + · refine le_of_eq_of_le ?_ <| smul_top_inf_eq_smul_of_isSMulRegular_on_quot <| + ha.of_injective _ <| ker_eq_bot.mp <| ker_liftQ_eq_bot' _ (lsmul R M b) rfl + rw [← (isSMulRegular_on_quot_iff_lsmul_comap_eq _ _).mp hb] + exact (inf_eq_right.mpr (ker_le_comap _)).symm + · rwa [ha.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, inf_comm, smul_comm, + ← h2.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, and_iff_left hb] + -- TODO: Equivalence of permutability of regular sequences to regularity of -- subsequences and regularity on poly ring. See [07DW] in stacks project -- We need a theory of multivariate polynomial modules first diff --git a/mathlib4/lakefile.lean b/mathlib4/lakefile.lean index 1c2f6bf57..c43ad638e 100644 --- a/mathlib4/lakefile.lean +++ b/mathlib4/lakefile.lean @@ -43,6 +43,7 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[ abbrev mathlibLeanOptions := #[ ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b` ⟨`autoImplicit, false⟩, + ⟨`backward.isDefEq.instanceTypes, "markOrSynth"⟩, ⟨`maxSynthPendingDepth, .ofNat 3⟩, ] ++ -- options that are used in `lake build` mathlibOnlyLinters.map fun s ↦ { s with name := `weak ++ s.name }