diff --git a/batteries/Batteries/Data/Fin/Coding.lean b/batteries/Batteries/Data/Fin/Coding.lean index 5d20ed0d4..e399794fa 100644 --- a/batteries/Batteries/Data/Fin/Coding.lean +++ b/batteries/Batteries/Data/Fin/Coding.lean @@ -106,6 +106,7 @@ def encodeChar (c : Char) : Fin Char.count := else Char.ofNatAux (i.val + (Char.maxSurrogate + 1 - Char.minSurrogate)) (by grind) +set_option dsimp.resynthInstances false in @[simp] theorem encodeChar_decodeChar (x) : encodeChar (decodeChar x) = x := by simp only [decodeChar, encodeChar] split @@ -113,6 +114,7 @@ def encodeChar (c : Char) : Fin Char.count := · have : ¬ x.val + (Char.maxSurrogate + 1 - Char.minSurrogate) < Char.minSurrogate := by grind simp [*] +set_option dsimp.resynthInstances false in @[simp] theorem decodeChar_encodeChar (x) : decodeChar (encodeChar x) = x := by ext; simp only [decodeChar, encodeChar] split diff --git a/batteries/Batteries/Data/Int.lean b/batteries/Batteries/Data/Int.lean index 0b6de9782..c57de042c 100644 --- a/batteries/Batteries/Data/Int.lean +++ b/batteries/Batteries/Data/Int.lean @@ -42,6 +42,7 @@ def ofBits (f : Fin n → Bool) := · have hlt := Nat.ofBits_lt_two_pow f simp [subNatNat_of_lt hlt, testBit, Nat.sub_sub, Nat.testBit_two_pow_sub_succ hlt, h] +set_option dsimp.resynthInstances false in @[simp] theorem testBit_ofBits_ge {f : Fin n → Bool} (h : i ≥ n) : (ofBits f).testBit i = decide (ofBits f < 0) := by simp only [ofBits] diff --git a/lean-toolchain b/lean-toolchain index aa3b71f65..80ece21ea 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-09-09 +leanprover/lean4-pr-releases:pr-release-15109-ae44bc8 diff --git a/mathlib4/Mathlib/Algebra/Category/AlgCat/FilteredColimits.lean b/mathlib4/Mathlib/Algebra/Category/AlgCat/FilteredColimits.lean index 456f2f2f3..30403c3b1 100644 --- a/mathlib4/Mathlib/Algebra/Category/AlgCat/FilteredColimits.lean +++ b/mathlib4/Mathlib/Algebra/Category/AlgCat/FilteredColimits.lean @@ -34,6 +34,7 @@ variable {c : Cocone (F ⋙ forget₂ _ RingCat)} [IsFilteredOrEmpty J] set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- (Implementation): The algebra instance on the cocone point of the underlying diagram of rings is induced from the `j`-th inclusion map. Any choice of `j` gives a propositionally equal algebra instance. -/ diff --git a/mathlib4/Mathlib/Algebra/Category/AlgCat/Limits.lean b/mathlib4/Mathlib/Algebra/Category/AlgCat/Limits.lean index 598e16667..071e40ad1 100644 --- a/mathlib4/Mathlib/Algebra/Category/AlgCat/Limits.lean +++ b/mathlib4/Mathlib/Algebra/Category/AlgCat/Limits.lean @@ -70,6 +70,7 @@ instance limitAlgebra : inferInstanceAs <| Algebra R (Shrink (sectionsSubalgebra F)) set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- `limit.π (F ⋙ forget (AlgCat R)) j` as an `AlgHom`. -/ def limitπAlgHom (j) : (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt →ₐ[R] diff --git a/mathlib4/Mathlib/Algebra/Category/AlgCat/TensorAlgebra.lean b/mathlib4/Mathlib/Algebra/Category/AlgCat/TensorAlgebra.lean index 1a1f307a2..8d6d3376d 100644 --- a/mathlib4/Mathlib/Algebra/Category/AlgCat/TensorAlgebra.lean +++ b/mathlib4/Mathlib/Algebra/Category/AlgCat/TensorAlgebra.lean @@ -37,6 +37,7 @@ variable (R : Type u) [CommRing R] set_option backward.isDefEq.respectTransparency false in set_option backward.defeqAttrib.useBackward true in +set_option dsimp.resynthInstances false in /-- Taking the tensor algebra forms a left adjoint of the forgetful functor from `AlgCat R` to `ModuleCat R`. -/ @[simps] diff --git a/mathlib4/Mathlib/Algebra/Category/Grp/Colimits.lean b/mathlib4/Mathlib/Algebra/Category/Grp/Colimits.lean index 605a75656..4ffdd053d 100644 --- a/mathlib4/Mathlib/Algebra/Category/Grp/Colimits.lean +++ b/mathlib4/Mathlib/Algebra/Category/Grp/Colimits.lean @@ -129,6 +129,7 @@ lemma quotToQuotUlift_ι [DecidableEq J] (j : J) (x : F.obj j) : set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The obvious additive map from `Quot (F ⋙ uliftFunctor.{u'})` to `Quot F`. -/ diff --git a/mathlib4/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean b/mathlib4/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean index 4304522f7..b2abd4158 100644 --- a/mathlib4/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean +++ b/mathlib4/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean @@ -75,6 +75,7 @@ open scoped MonObj set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in attribute [-instance] Functor.LaxMonoidal.comp Functor.Monoidal.instComp in +set_option dsimp.resynthInstances false in /-- Implementation, see `leftExactFunctorForgetEquivalence`. This is the complicated bit, where we show that forgetting the group structure in the image of `F` and then reconstructing it recovers the group structure we started with. -/ diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean index 2d836e012..71fb7d9ae 100644 --- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean +++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean @@ -115,6 +115,7 @@ differential map `B → KaehlerDifferential f`. -/ noncomputable abbrev d (b : B) : KaehlerDifferential f := (D f).d b set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in @[ext] lemma ext {M : ModuleCat B} {α β : KaehlerDifferential f ⟶ M} (h : ∀ (b : B), α (d b) = β (d b)) : α = β := by diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Kernels.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Kernels.lean index 0104f495e..a09c15e69 100644 --- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Kernels.lean +++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Kernels.lean @@ -44,6 +44,7 @@ def kernelIsLimit : IsLimit (kernelCone f) := set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Construct an `IsLimit` structure of kernels given `Function.Exact`. -/ noncomputable def isLimitKernelFork (f : M ⟶ N) (g : N ⟶ P) (H : Function.Exact f.hom g.hom) diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean index 5f3e34bdc..9cef8524f 100644 --- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean +++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf.lean @@ -213,6 +213,7 @@ lemma ofPresheaf_presheaf : (ofPresheaf M map_smul).presheaf = M := rfl end set_option backward.isDefEq.respectTransparency.types false in +set_option dsimp.resynthInstances false in /-- The morphism of presheaves of modules `M₁ ⟶ M₂` given by a morphism of abelian presheaves `M₁.presheaf ⟶ M₂.presheaf` which satisfy a suitable linearity condition. -/ diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean index 3448fb456..45472b29a 100644 --- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean +++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean @@ -74,6 +74,7 @@ noncomputable def freeObjDesc (φ : F ⟶ G.presheaf ⋙ forget _) : freeObj F set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in variable (F R) in +set_option dsimp.resynthInstances false in /-- The unit of `PresheafOfModules.freeAdjunction`. -/ @[simps] noncomputable def freeAdjunctionUnit : F ⟶ (freeObj (R := R) F).presheaf ⋙ forget _ where @@ -82,6 +83,7 @@ noncomputable def freeAdjunctionUnit : F ⟶ (freeObj (R := R) F).presheaf ⋙ f set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The bijection `(freeObj F ⟶ G) ≃ (F ⟶ G.presheaf ⋙ forget _)` when `F` is a presheaf of types and `G` a presheaf of modules. -/ noncomputable def freeHomEquiv : (freeObj F ⟶ G) ≃ (F ⟶ G.presheaf ⋙ forget _) where @@ -98,6 +100,7 @@ lemma free_hom_ext {ψ ψ' : freeObj F ⟶ G} set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in variable (R) in +set_option dsimp.resynthInstances false in /-- The free presheaf of modules functor is left adjoint to the forget functor `PresheafOfModules.{u} R ⥤ Cᵒᵖ ⥤ Type u`. -/ noncomputable def freeAdjunction : diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean index e32a93670..2df363e2f 100644 --- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean +++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean @@ -412,6 +412,7 @@ def freeObj (X : TopCat.{v}) : TopModuleCat.{max v u} R := lemma coe_freeObj (X : TopCat.{v}) : freeObj R X = (X →₀ R) := rfl set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The free topological module over a topological space is functorial. -/ noncomputable def freeMap {X Y : TopCat.{v}} (f : X ⟶ Y) : freeObj R X ⟶ freeObj R Y := @@ -442,6 +443,7 @@ def free : TopCat.{v} ⥤ TopModuleCat.{max v u} R := set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The free-forgetful adjoint for `TopModuleCat R`. -/ noncomputable def freeAdj : free.{max v u} R ⊣ forget₂ (TopModuleCat.{max v u} R) TopCat.{max v u} where diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Ulift.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Ulift.lean index 07439723c..e901d0710 100644 --- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Ulift.lean +++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Ulift.lean @@ -75,6 +75,7 @@ instance : Limits.PreservesFiniteLimits (uliftFunctor.{v', v} R) := set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in lemma uliftFunctor_map_exact (S : ShortComplex (ModuleCat.{v} R)) (h : S.Exact) : (S.map (uliftFunctor R)).Exact := by rw [CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact] diff --git a/mathlib4/Mathlib/Algebra/Category/MonCat/Adjunctions.lean b/mathlib4/Mathlib/Algebra/Category/MonCat/Adjunctions.lean index d6dee2dde..32c7d1193 100644 --- a/mathlib4/Mathlib/Algebra/Category/MonCat/Adjunctions.lean +++ b/mathlib4/Mathlib/Algebra/Category/MonCat/Adjunctions.lean @@ -96,6 +96,7 @@ def free : Type u ⥤ AddCommMonCat.{u} where set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The free-forgetful adjunction for commutative monoids. -/ noncomputable def adj : free ⊣ forget AddCommMonCat.{u} where diff --git a/mathlib4/Mathlib/Algebra/Category/Ring/Under/Property.lean b/mathlib4/Mathlib/Algebra/Category/Ring/Under/Property.lean index d58aa6579..d52b6c348 100644 --- a/mathlib4/Mathlib/Algebra/Category/Ring/Under/Property.lean +++ b/mathlib4/Mathlib/Algebra/Category/Ring/Under/Property.lean @@ -141,6 +141,7 @@ open RingHom variable {P} +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency.types false in set_option backward.defeqAttrib.useBackward true in lemma CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijective diff --git a/mathlib4/Mathlib/Algebra/GroupWithZero/Indicator.lean b/mathlib4/Mathlib/Algebra/GroupWithZero/Indicator.lean index c648e0f33..88608aa67 100644 --- a/mathlib4/Mathlib/Algebra/GroupWithZero/Indicator.lean +++ b/mathlib4/Mathlib/Algebra/GroupWithZero/Indicator.lean @@ -68,6 +68,7 @@ variable [MulZeroOneClass M₀] {s t : Set ι} {i : ι} lemma inter_indicator_one : (s ∩ t).indicator (1 : ι → M₀) = s.indicator 1 * t.indicator 1 := funext fun _ ↦ by simp only [← inter_indicator_mul, Pi.mul_apply, Pi.one_apply, one_mul]; congr +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in lemma indicator_prod_one {t : Set κ} {j : κ} : (s ×ˢ t).indicator (1 : ι × κ → M₀) (i, j) = s.indicator 1 i * t.indicator 1 j := by diff --git a/mathlib4/Mathlib/Algebra/Homology/DerivedCategory/Basic.lean b/mathlib4/Mathlib/Algebra/Homology/DerivedCategory/Basic.lean index 7402a1854..ce8e5bc52 100644 --- a/mathlib4/Mathlib/Algebra/Homology/DerivedCategory/Basic.lean +++ b/mathlib4/Mathlib/Algebra/Homology/DerivedCategory/Basic.lean @@ -95,6 +95,7 @@ variable {C} def Q : CochainComplex C ℤ ⥤ DerivedCategory C := HomologicalComplexUpToQuasiIso.Q set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in instance : (Q (C := C)).IsLocalization (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) := by dsimp only [Q, DerivedCategory] @@ -129,6 +130,7 @@ lemma quotientCompQhIso_inv_naturality {K L : CochainComplex C ℤ} (f : K ⟶ L (quotientCompQhIso C).inv.naturality f set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in instance : Qh.IsLocalization (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) := by dsimp [Qh, DerivedCategory] infer_instance diff --git a/mathlib4/Mathlib/Algebra/Homology/HomotopyCategory/Plus.lean b/mathlib4/Mathlib/Algebra/Homology/HomotopyCategory/Plus.lean index bd5bb7a00..74d111d55 100644 --- a/mathlib4/Mathlib/Algebra/Homology/HomotopyCategory/Plus.lean +++ b/mathlib4/Mathlib/Algebra/Homology/HomotopyCategory/Plus.lean @@ -297,6 +297,7 @@ noncomputable instance : F.mapHomotopyCategory (.up ℤ)) _).CommShift ℤ) set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in instance [HasZeroObject C] [HasBinaryBiproducts C] [HasZeroObject D] [HasBinaryBiproducts D] : (F.mapHomotopyCategoryPlus).IsTriangulated := by dsimp only [mapHomotopyCategoryPlus] diff --git a/mathlib4/Mathlib/Algebra/Lie/UniversalEnveloping.lean b/mathlib4/Mathlib/Algebra/Lie/UniversalEnveloping.lean index 8ebf54ba4..05b9b4460 100644 --- a/mathlib4/Mathlib/Algebra/Lie/UniversalEnveloping.lean +++ b/mathlib4/Mathlib/Algebra/Lie/UniversalEnveloping.lean @@ -87,6 +87,7 @@ def ι : L →ₗ⁅R⁆ UniversalEnvelopingAlgebra R L := variable {A : Type u₃} [Ring A] [Algebra R A] (f : L →ₗ⁅R⁆ A) set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The universal property of the universal enveloping algebra: Lie algebra morphisms into associative algebras lift to associative algebra morphisms from the universal enveloping algebra. -/ def lift : (L →ₗ⁅R⁆ A) ≃ (UniversalEnvelopingAlgebra R L →ₐ[R] A) where diff --git a/mathlib4/Mathlib/Algebra/Module/Presentation/Differentials.lean b/mathlib4/Mathlib/Algebra/Module/Presentation/Differentials.lean index d435719b3..d408ed88c 100644 --- a/mathlib4/Mathlib/Algebra/Module/Presentation/Differentials.lean +++ b/mathlib4/Mathlib/Algebra/Module/Presentation/Differentials.lean @@ -72,12 +72,14 @@ lemma comm₂₃' : pres.toExtension.toKaehler.comp pres.cotangentSpaceBasis.rep ext simp +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The canonical map `(σ →₀ S) →ₗ[S] pres.toExtension.Cotangent`. -/ noncomputable def hom₁ : (σ →₀ S) →ₗ[S] pres.toExtension.Cotangent := Finsupp.linearCombination S (fun r ↦ Extension.Cotangent.mk ⟨pres.relation r, by simp⟩) +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma hom₁_single (r : σ) : @@ -109,6 +111,7 @@ the transparency bump that instance-implicit arguments would otherwise receive. Potential fix: Mark `Generators.toExtension` implicit-reducible; then `respectTransparency false` and `instanceSearchTypes false` can both go. -/ +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency.instanceSearchTypes false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in @@ -138,6 +141,7 @@ lemma surjective_hom₁ : Function.Surjective (hom₁ pres) := by simp only [LinearMap.coe_mk, AddHom.coe_mk, hom₁_single, φ] rfl +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma comm₁₂_single (r : σ) : diff --git a/mathlib4/Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean b/mathlib4/Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean index 121b83814..6fd2a8b7b 100644 --- a/mathlib4/Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean +++ b/mathlib4/Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean @@ -465,6 +465,7 @@ theorem mul_sum {S : Type*} [NonUnitalNonAssocSemiring S] (b : S) (s : SkewMonoi simp only [sum, Finsupp.sum, Finset.mul_sum] set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Analogue of `Finsupp.sum_ite_eq'` for `SkewMonoidAlgebra`. -/ @[deprecated Finsupp.sum_ite_eq' +typeChanged (since := "2026-07-04")] theorem sum_ite_eq' {N : Type*} [AddCommMonoid N] [DecidableEq G] (f : SkewMonoidAlgebra k G) diff --git a/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/UnionProd.lean b/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/UnionProd.lean index 399b6cf85..5bce01fb4 100644 --- a/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/UnionProd.lean +++ b/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/UnionProd.lean @@ -100,6 +100,7 @@ lemma isIndex_succ (l : Fin d) : (x.cast hd).simplex.1 l.succ = k.succ ∧ (x.cast hd).simplex.2 l.succ = (x.cast hd).simplex.2 l.castSucc := Iff.rfl +set_option dsimp.resynthInstances false in lemma mem_range_left (i : Fin (m + 2)) (hi : i ≠ k.castSucc) : i ∈ Set.range (x.cast hd).simplex.1 := by subst hd @@ -107,6 +108,7 @@ lemma mem_range_left (i : Fin (m + 2)) (hi : i ≠ k.castSucc) : simp [Subcomplex.mem_unionProd_iff, mem_horn_iff_notMem_range] at this tauto +set_option dsimp.resynthInstances false in lemma mem_range_right (i : Fin (n + 1)) : i ∈ Set.range (x.cast hd).simplex.2 := by subst hd @@ -206,6 +208,7 @@ variable {x} {hd : x.dim = d + 1} {l : Fin (d + 1)} (hl : IsIndex x hd l.succ) include hl +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency.types false in /-- The type (II) simplex obtained as a face of a type (I) simplex. -/ @[simps -isSimp] diff --git a/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/Homotopy.lean b/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/Homotopy.lean index 22770aa52..a5b6bec47 100644 --- a/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/Homotopy.lean +++ b/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/Homotopy.lean @@ -63,6 +63,7 @@ lemma h₁ (H : Homotopy f g) : ι₁ ≫ H.h = g := RelativeMorphism.Homotopy.h₁ H set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- If `H : Homotopy f g` is a homotopy between morphisms of simplicial sets `f : X ⟶ Y` and `g : X ⟶ Y` (i.e. `H.h` is a morphism `X ⊗ Δ[1] ⟶ Y` inducing `f` and `g`), then this is the corresponding (combinatorial) homotopy of diff --git a/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean b/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean index 49489373d..2b63d1dc5 100644 --- a/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean +++ b/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean @@ -248,6 +248,7 @@ variable {X Y : SSet.{u}} (S : X.Subcomplex) (T : Y.Subcomplex) /-- Given `S ≤ X` and `T ≤ Y`, this is the subcomplex of `X ⊗ Y` given by `(X ⊗ T) ⊔ (S ⊗ Y)`. -/ def unionProd : (X ⊗ Y).Subcomplex := ((⊤ : X.Subcomplex).prod T) ⊔ (S.prod ⊤) +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in lemma mem_unionProd_iff {n : SimplexCategoryᵒᵖ} (x : (X ⊗ Y).obj n) : dsimp% x ∈ (unionProd S T).obj _ ↔ x.2 ∈ T.obj _ ∨ x.1 ∈ S.obj _ := by @@ -304,6 +305,7 @@ lemma isPushout : IsPushout (S.ι ▷ (T : SSet)) ((S : SSet) ◁ T.ι) (prodIso _ _ ≪≫ whiskerLeftIso _ (topIso Y)) (Iso.refl _) rfl rfl rfl rfl +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency.types false in @[simp] lemma preimage_β_hom : (unionProd S T).preimage (β_ _ _).hom = unionProd T S := by diff --git a/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplexOne.lean b/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplexOne.lean index 29e4d51f3..1d2a5b8e4 100644 --- a/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplexOne.lean +++ b/mathlib4/Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplexOne.lean @@ -99,6 +99,7 @@ lemma ofSimplex_le_filtration {i j : Fin (p + 1)} (hij : i ≤ j) : Subcomplex.ofSimplex (nonDegenerateEquiv i.val).val) ⟨i, hij⟩ variable (p) in +set_option dsimp.resynthInstances false in lemma filtration_zero : filtration.{u} (0 : Fin (p + 1)) = .ofSimplex (nonDegenerateEquiv 0).val := le_antisymm (by simp [filtration]) (ofSimplex_le_filtration.{u} (by rfl)) diff --git a/mathlib4/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean b/mathlib4/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean index 633c4dec6..6ff5c4236 100644 --- a/mathlib4/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean +++ b/mathlib4/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean @@ -1047,6 +1047,7 @@ private lemma faaDiBruno_aux2 {m : ℕ} (q : FormalMultilinearSeries 𝕜 F G) set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- *Faa di Bruno* formula: If two functions `g` and `f` have Taylor series up to `n` given by `q` and `p`, then `g ∘ f` also has a Taylor series, given by `q.taylorComp p`. -/ theorem HasFTaylorSeriesUpToOn.comp {n : WithTop ℕ∞} {g : F → G} {f : E → F} diff --git a/mathlib4/Mathlib/Analysis/Calculus/IteratedDeriv/FaaDiBruno.lean b/mathlib4/Mathlib/Analysis/Calculus/IteratedDeriv/FaaDiBruno.lean index 3d2647ba3..3faf008b5 100644 --- a/mathlib4/Mathlib/Analysis/Calculus/IteratedDeriv/FaaDiBruno.lean +++ b/mathlib4/Mathlib/Analysis/Calculus/IteratedDeriv/FaaDiBruno.lean @@ -63,6 +63,7 @@ theorem iteratedDeriv_vcomp_eq_sum_orderedFinpartition uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _) hi set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in theorem iteratedDerivWithin_vcomp_two (hg : ContDiffWithinAt 𝕜 2 g t (f x)) (hf : ContDiffWithinAt 𝕜 2 f s x) (ht : UniqueDiffOn 𝕜 t) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hst : MapsTo f s t) : @@ -86,6 +87,7 @@ theorem iteratedDeriv_vcomp_two (hg : ContDiffAt 𝕜 2 g (f x)) (hf : ContDiffA exact iteratedDerivWithin_vcomp_two hg hf uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ x) (mapsTo_univ f _) +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in theorem iteratedDerivWithin_vcomp_three diff --git a/mathlib4/Mathlib/Analysis/Convex/Visible.lean b/mathlib4/Mathlib/Analysis/Convex/Visible.lean index 9d475f297..f598f295b 100644 --- a/mathlib4/Mathlib/Analysis/Convex/Visible.lean +++ b/mathlib4/Mathlib/Analysis/Convex/Visible.lean @@ -188,6 +188,7 @@ lemma IsClosed.convexHull_subset_affineSpan_isVisible (hs : IsClosed (convexHull hxz.mem_convexHull_isVisible hx hz) (ne_of_mem_of_not_mem hz hx).symm open Submodule in +set_option dsimp.resynthInstances false in /-- If `s` is a closed set of dimension `d` and `x` is a point outside of its convex hull, then `x` sees at least `d` points of the convex hull of `s` that actually lie in `s`. -/ lemma rank_le_card_isVisible (hs : IsClosed (convexHull ℝ s)) (hx : x ∉ convexHull ℝ s) : diff --git a/mathlib4/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/mathlib4/Mathlib/Analysis/InnerProductSpace/PiL2.lean index c718f6293..99d2fe205 100644 --- a/mathlib4/Mathlib/Analysis/InnerProductSpace/PiL2.lean +++ b/mathlib4/Mathlib/Analysis/InnerProductSpace/PiL2.lean @@ -259,6 +259,7 @@ def DirectSum.IsInternal.isometryL2OfOrthogonalFamily [DecidableEq ι] {V : ι · congr <;> simp set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in @[simp] theorem DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V) diff --git a/mathlib4/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/GabrielPopescu.lean b/mathlib4/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/GabrielPopescu.lean index 8574ee8a8..90e1fdac8 100644 --- a/mathlib4/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/GabrielPopescu.lean +++ b/mathlib4/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/GabrielPopescu.lean @@ -123,6 +123,7 @@ theorem GabrielPopescu.full (G : C) (hG : IsSeparator G) : (preadditiveCoyonedaO ext q simpa [-comp_epiDesc] using! Sigma.ι _ q ≫= comp_epiDesc _ _ h +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in theorem GabrielPopescu.preservesInjectiveObjects (G : C) (hG : IsSeparator G) : diff --git a/mathlib4/Mathlib/CategoryTheory/Bicategory/Functor/Oplax.lean b/mathlib4/Mathlib/CategoryTheory/Bicategory/Functor/Oplax.lean index f043a3f61..2ab75fd79 100644 --- a/mathlib4/Mathlib/CategoryTheory/Bicategory/Functor/Oplax.lean +++ b/mathlib4/Mathlib/CategoryTheory/Bicategory/Functor/Oplax.lean @@ -172,6 +172,7 @@ lemma mapComp'_eq_mapComp {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Composition of oplax functors. -/ --@[simps] def comp (F : B ⥤ᵒᵖᴸ C) (G : C ⥤ᵒᵖᴸ D) : B ⥤ᵒᵖᴸ D where diff --git a/mathlib4/Mathlib/CategoryTheory/Bicategory/Yoneda.lean b/mathlib4/Mathlib/CategoryTheory/Bicategory/Yoneda.lean index 771a1f527..9ae7d4ae8 100644 --- a/mathlib4/Mathlib/CategoryTheory/Bicategory/Yoneda.lean +++ b/mathlib4/Mathlib/CategoryTheory/Bicategory/Yoneda.lean @@ -93,6 +93,7 @@ def yoneda₀ (x : B) : Pseudofunctor Bᵒᵖ Cat.{w, v} where set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Postcomposing of a 1-morphism seen as a strong transformation between pseudofunctors. -/ @[simps!] def postcomp₂ {a b : B} (f : a ⟶ b) : yoneda₀ a ⟶ yoneda₀ b where @@ -112,6 +113,7 @@ def postcomposing₂ (a b : B) : (a ⟶ b) ⥤ (yoneda₀ a ⟶ yoneda₀ b) whe set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The Yoneda pseudofunctor from `B` to `Bᵒᵖ ⥤ᵖ Cat`. It consists of the following: diff --git a/mathlib4/Mathlib/CategoryTheory/Category/Cat/Limit.lean b/mathlib4/Mathlib/CategoryTheory/Category/Cat/Limit.lean index 049c8fa5d..e55ca4680 100644 --- a/mathlib4/Mathlib/CategoryTheory/Category/Cat/Limit.lean +++ b/mathlib4/Mathlib/CategoryTheory/Category/Cat/Limit.lean @@ -137,6 +137,7 @@ theorem limit_π_homDiagram_eqToHom {F : J ⥤ Cat.{v, v}} (X Y : limit (F ⋙ C set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Auxiliary definition: the proposed cone is a limit cone. -/ def limitConeIsLimit (F : J ⥤ Cat.{v, v}) : IsLimit (limitCone F) where lift := limitConeLift F diff --git a/mathlib4/Mathlib/CategoryTheory/Comma/StructuredArrow/Functor.lean b/mathlib4/Mathlib/CategoryTheory/Comma/StructuredArrow/Functor.lean index 551c20bb4..34e5be214 100644 --- a/mathlib4/Mathlib/CategoryTheory/Comma/StructuredArrow/Functor.lean +++ b/mathlib4/Mathlib/CategoryTheory/Comma/StructuredArrow/Functor.lean @@ -60,6 +60,7 @@ def functor (T : C ⥤ D) : D ⥤ Cat where variable {E : Type u₃} [Category.{v₃} E] variable (L : C ⥤ D) (R : E ⥤ D) +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The functor used to establish the equivalence `grothendieckPrecompFunctorEquivalence` between @@ -71,6 +72,7 @@ def grothendieckPrecompFunctorToComma : Grothendieck (R ⋙ functor L) ⥤ Comma set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Fibers of `grothendieckPrecompFunctorToComma L R`, composed with `Comma.fst L R`, are isomorphic to the projection `proj L (R.obj X)`. -/ @[simps!] @@ -79,6 +81,7 @@ def ιCompGrothendieckPrecompFunctorToCommaCompFst (X : E) : proj L (R.obj X) := NatIso.ofComponents (fun X => Iso.refl _) (fun _ => by simp) +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The inverse functor used to establish the equivalence `grothendieckPrecompFunctorEquivalence` diff --git a/mathlib4/Mathlib/CategoryTheory/FintypeCat.lean b/mathlib4/Mathlib/CategoryTheory/FintypeCat.lean index d6b3a07aa..006f411a2 100644 --- a/mathlib4/Mathlib/CategoryTheory/FintypeCat.lean +++ b/mathlib4/Mathlib/CategoryTheory/FintypeCat.lean @@ -236,6 +236,7 @@ noncomputable instance : incl.IsEquivalence where noncomputable def equivalence : Skeleton ≌ FintypeCat := incl.asEquivalence +set_option dsimp.resynthInstances false in attribute [local instance] FintypeCat.fintype in @[simp] theorem incl_mk_nat_card (n : ℕ) : diff --git a/mathlib4/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean b/mathlib4/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean index 7ea6c4382..517080132 100644 --- a/mathlib4/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean +++ b/mathlib4/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean @@ -119,6 +119,7 @@ theorem hasColimit_map_comp_ι_comp_grothendieckProj {X Y : D} (f : X ⟶ Y) : grothendieckProj L ⋙ F) := hasColimit_of_iso (isoWhiskerRight (mapCompιCompGrothendieckProj L f) F) +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in /-- The left Kan extension of `F : C ⥤ H` along a functor `L : C ⥤ D` is isomorphic to the fiberwise colimit of the projection functor on the Grothendieck construction of the costructured @@ -229,6 +230,7 @@ noncomputable def colimitIsoColimitGrothendieck : _ ≅ colimit (CostructuredArrow.grothendieckProj L ⋙ G) := colimitFiberwiseColimitIso _ +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in @[reassoc (attr := simp)] lemma ι_colimitIsoColimitGrothendieck_inv (X : Grothendieck (CostructuredArrow.functor L)) : diff --git a/mathlib4/Mathlib/CategoryTheory/Grothendieck.lean b/mathlib4/Mathlib/CategoryTheory/Grothendieck.lean index f4e8b142a..42226b15f 100644 --- a/mathlib4/Mathlib/CategoryTheory/Grothendieck.lean +++ b/mathlib4/Mathlib/CategoryTheory/Grothendieck.lean @@ -320,6 +320,7 @@ def compAsSmallFunctorEquivalenceInverse : set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The functor to build the equivalence `compAsSmallFunctorEquivalence`. -/ @[simps] def compAsSmallFunctorEquivalenceFunctor : @@ -341,6 +342,7 @@ def compAsSmallFunctorEquivalence : counitIso := Iso.refl _ unitIso := Iso.refl _ +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in variable {F} in diff --git a/mathlib4/Mathlib/CategoryTheory/Groupoid/FreeGroupoidOfCategory.lean b/mathlib4/Mathlib/CategoryTheory/Groupoid/FreeGroupoidOfCategory.lean index daf6be49e..ca931a735 100644 --- a/mathlib4/Mathlib/CategoryTheory/Groupoid/FreeGroupoidOfCategory.lean +++ b/mathlib4/Mathlib/CategoryTheory/Groupoid/FreeGroupoidOfCategory.lean @@ -286,6 +286,7 @@ namespace Grpd open FreeGroupoid set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The free groupoid construction on a category as a functor. -/ def free : Cat.{u, u} ⥤ Grpd.{u, u} where obj C := ↧(FreeGroupoid C) diff --git a/mathlib4/Mathlib/CategoryTheory/Groupoid/Grpd/Basic.lean b/mathlib4/Mathlib/CategoryTheory/Groupoid/Grpd/Basic.lean index b741cca1c..30bf029c4 100644 --- a/mathlib4/Mathlib/CategoryTheory/Groupoid/Grpd/Basic.lean +++ b/mathlib4/Mathlib/CategoryTheory/Groupoid/Grpd/Basic.lean @@ -107,6 +107,7 @@ def piLimitFan ⦃J : Type u⦄ (F : J → Grpd.{u, u}) : Limits.Fan F := set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The product fan over an indexed family of groupoids, is a limit cone. -/ def piLimitFanIsLimit ⦃J : Type u⦄ (F : J → Grpd.{u, u}) : Limits.IsLimit (piLimitFan F) := Limits.Fan.IsLimit.mk (piLimitFan F) (fun s => Functor.pi' fun j => s.proj j) diff --git a/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean b/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean index e045d1973..06d43e89d 100644 --- a/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean +++ b/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean @@ -267,6 +267,7 @@ variable [ConcreteCategory.{s} C FC] set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in theorem multiequalizer_ext {J : MulticospanShape.{w, w'}} {I : MulticospanIndex J C} [HasMultiequalizer I] [PreservesLimit I.multicospan (forget C)] (x y : ToType (multiequalizer I)) diff --git a/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/Basic.lean b/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/Basic.lean index ef3eae454..f726858f0 100644 --- a/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/Basic.lean +++ b/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/Basic.lean @@ -513,6 +513,7 @@ variable {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The construction `CatCommSqOver.transform` respects vertical composition of `CatCospanTransform`s. -/ @[simps!] @@ -527,6 +528,7 @@ def transformObjComp (X : Type u₁₀) [Category.{v₁₀} X] set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The construction `CatCommSqOver.transform` respects the identity `CatCospanTransform`s. -/ @[simps!] diff --git a/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform.lean b/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform.lean index 8aca996e3..8e252ddf3 100644 --- a/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform.lean +++ b/mathlib4/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform.lean @@ -178,6 +178,7 @@ lemma right_coherence_app {ψ ψ' : CatCospanTransform F G F' G'} set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Whiskering left of a `CatCospanTransformMorphism` by a `CatCospanTransform`. -/ @[simps] def whiskerLeft (φ : CatCospanTransform F G F' G') @@ -189,6 +190,7 @@ def whiskerLeft (φ : CatCospanTransform F G F' G') set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Whiskering right of a `CatCospanTransformMorphism` by a `CatCospanTransform`. -/ @[simps] def whiskerRight {ψ ψ' : CatCospanTransform F G F' G'} (α : ψ ⟶ ψ') @@ -318,6 +320,7 @@ end Iso set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The left unitor isomorphism for categorical cospan transformations. -/ @[simps!] def leftUnitor (φ : CatCospanTransform F G F' G') : @@ -326,6 +329,7 @@ def leftUnitor (φ : CatCospanTransform F G F' G') : set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The right unitor isomorphism for categorical cospan transformations. -/ @[simps!] def rightUnitor (φ : CatCospanTransform F G F' G') : @@ -334,6 +338,7 @@ def rightUnitor (φ : CatCospanTransform F G F' G') : set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The associator isomorphism for categorical cospan transformations. -/ @[simps!] def associator {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂} diff --git a/mathlib4/Mathlib/CategoryTheory/Monoidal/Bimon_.lean b/mathlib4/Mathlib/CategoryTheory/Monoidal/Bimon_.lean index 174e038cc..802d239c4 100644 --- a/mathlib4/Mathlib/CategoryTheory/Monoidal/Bimon_.lean +++ b/mathlib4/Mathlib/CategoryTheory/Monoidal/Bimon_.lean @@ -109,6 +109,7 @@ def toMonComonObj (M : Bimon C) : Mon (Comon C) where mon.mul.hom := μ[M.X.X] mon.mul.isComonHom_hom.hom_comul := by simp +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency.types false in /-- The forward direction of `Comon (Mon C) ≌ Mon (Comon C)` -/ @[simps] @@ -142,6 +143,7 @@ def ofMonComonObj (M : Mon (Comon C)) : Bimon C where comon.counit := .mk' ε[M.X.X] comon.comul := .mk' Δ[M.X.X] +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency.types false in variable (C) in /-- The backward direction of `Comon (Mon C) ≌ Mon (Comon C)` -/ diff --git a/mathlib4/Mathlib/CategoryTheory/Monoidal/Cartesian/Ring.lean b/mathlib4/Mathlib/CategoryTheory/Monoidal/Cartesian/Ring.lean index cfae3174b..858137cd3 100644 --- a/mathlib4/Mathlib/CategoryTheory/Monoidal/Cartesian/Ring.lean +++ b/mathlib4/Mathlib/CategoryTheory/Monoidal/Cartesian/Ring.lean @@ -41,6 +41,7 @@ set_option backward.defeqAttrib.useBackward true in lemma yonedaRingObj_map_apply {R : C} [RingObj R] {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : X.unop ⟶ R) : dsimp% (yonedaRingObj R).map f x = f.unop ≫ x := rfl +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The yoneda embedding of `RingObjCat C` into presheaves of rings. -/ @@ -65,6 +66,7 @@ set_option backward.defeqAttrib.useBackward true in lemma yonedaCommRingObj_map_apply {R : C} [CommRingObj R] {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : X.unop ⟶ R) : dsimp% (yonedaCommRingObj R).map f x = f.unop ≫ x := rfl +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The yoneda embedding of `CommRingObjCat C` into presheaves of commutative rings. -/ diff --git a/mathlib4/Mathlib/CategoryTheory/Monoidal/Cartesian/ShrinkYoneda.lean b/mathlib4/Mathlib/CategoryTheory/Monoidal/Cartesian/ShrinkYoneda.lean index 1c85a0fd1..e09d2654c 100644 --- a/mathlib4/Mathlib/CategoryTheory/Monoidal/Cartesian/ShrinkYoneda.lean +++ b/mathlib4/Mathlib/CategoryTheory/Monoidal/Cartesian/ShrinkYoneda.lean @@ -37,6 +37,7 @@ instance (M : Grp C) (X : Cᵒᵖ) : Small.{w} ((yonedaGrp.obj M).obj X) := by dsimp infer_instance +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The Yoneda embedding `Mon C ⥤ Cᵒᵖ ⥤ MonCat.{w}` for a locally `w`-small category `C`. -/ @@ -53,6 +54,7 @@ noncomputable def shrinkYonedaMonObjObjEquiv {M : Mon C} {Y : Cᵒᵖ} : (shrinkYonedaMon.{w}.obj M).obj Y ≃* (Y.unop ⟶ M.X) := Shrink.mulEquiv +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma shrinkYonedaMon_obj_map_shrinkYonedaMonObjObjEquiv_symm @@ -66,6 +68,7 @@ lemma shrinkYonedaMonObjObjEquiv_symm_comp {M : Mon C} {Y Y' : C} (g : Y' ⟶ Y) (shrinkYonedaMon.obj _).map g.op (shrinkYonedaMonObjObjEquiv.symm f) := (shrinkYonedaMon_obj_map_shrinkYonedaMonObjObjEquiv_symm g.op f).symm +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma shrinkYonedaMon_map_app_shrinkYonedaObjObjEquiv_symm @@ -74,6 +77,7 @@ lemma shrinkYonedaMon_map_app_shrinkYonedaObjObjEquiv_symm shrinkYonedaMonObjObjEquiv.symm (f ≫ g.hom) := by simp [shrinkYonedaMon, shrinkYonedaMonObjObjEquiv] +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The Yoneda embedding `Grp C ⥤ Cᵒᵖ ⥤ GrpCat.{w}` for a locally `w`-small category `C`. -/ @@ -88,6 +92,7 @@ noncomputable def shrinkYonedaGrpObjObjEquiv {M : Grp C} {Y : Cᵒᵖ} : (shrinkYonedaGrp.{w}.obj M).obj Y ≃* (Y.unop ⟶ M.X) := Shrink.mulEquiv +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma shrinkYonedaGrp_obj_map_shrinkYonedaGrpObjObjEquiv_symm @@ -101,6 +106,7 @@ lemma shrinkYonedaGrpObjObjEquiv_symm_comp {M : Grp C} {Y Y' : C} (g : Y' ⟶ Y) (shrinkYonedaGrp.obj _).map g.op (shrinkYonedaGrpObjObjEquiv.symm f) := (shrinkYonedaGrp_obj_map_shrinkYonedaGrpObjObjEquiv_symm g.op f).symm +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma shrinkYonedaGrp_map_app_shrinkYonedaObjObjEquiv_symm diff --git a/mathlib4/Mathlib/CategoryTheory/Monoidal/Closed/FunctorCategory/Basic.lean b/mathlib4/Mathlib/CategoryTheory/Monoidal/Closed/FunctorCategory/Basic.lean index 6f3c9a844..b11f1b7fc 100644 --- a/mathlib4/Mathlib/CategoryTheory/Monoidal/Closed/FunctorCategory/Basic.lean +++ b/mathlib4/Mathlib/CategoryTheory/Monoidal/Closed/FunctorCategory/Basic.lean @@ -43,6 +43,7 @@ variable {F₁ F₂ F₂' F₃ F₃' : J ⥤ C} set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The bijection `(F₁ ⊗ F₂ ⟶ F₃) ≃ (F₂ ⟶ functorEnrichedHom C F₁ F₃)` when `F₁`, `F₂` and `F₃` are functors `J ⥤ C`, and `C` is monoidal closed. -/ noncomputable def homEquiv : (F₁ ⊗ F₂ ⟶ F₃) ≃ (F₂ ⟶ functorEnrichedHom C F₁ F₃) where @@ -90,6 +91,7 @@ noncomputable def homEquiv : (F₁ ⊗ F₂ ⟶ F₃) ≃ (F₂ ⟶ functorEnric simp set_option backward.isDefEq.respectTransparency.types false in +set_option dsimp.resynthInstances false in lemma homEquiv_naturality_two_symm (f₂ : F₂ ⟶ F₂') (g : F₂' ⟶ functorEnrichedHom C F₁ F₃) : homEquiv.symm (f₂ ≫ g) = F₁ ◁ f₂ ≫ homEquiv.symm g := by dsimp [homEquiv] @@ -98,6 +100,7 @@ lemma homEquiv_naturality_two_symm (f₂ : F₂ ⟶ F₂') (g : F₂' ⟶ functo set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in lemma homEquiv_naturality_three [∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂] (f : F₁ ⊗ F₂ ⟶ F₃) (f₃ : F₃ ⟶ F₃') : homEquiv (f ≫ f₃) = homEquiv f ≫ (ρ_ _).inv ≫ _ ◁ functorHomEquiv _ f₃ ≫ diff --git a/mathlib4/Mathlib/CategoryTheory/Monoidal/CommMon_.lean b/mathlib4/Mathlib/CategoryTheory/Monoidal/CommMon_.lean index bd4df3d1f..6ddf22dd1 100644 --- a/mathlib4/Mathlib/CategoryTheory/Monoidal/CommMon_.lean +++ b/mathlib4/Mathlib/CategoryTheory/Monoidal/CommMon_.lean @@ -325,6 +325,7 @@ variable (C) set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Implementation of `CommMon.equivLaxBraidedFunctorPUnit`. -/ @[simps] def commMonToLaxBraided : CommMon C ⥤ LaxBraidedFunctor (Discrete PUnit.{u + 1}) C where @@ -336,6 +337,7 @@ def commMonToLaxBraided : CommMon C ⥤ LaxBraidedFunctor (Discrete PUnit.{u + 1 set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Implementation of `CommMon.equivLaxBraidedFunctorPUnit`. -/ @[simps!] def unitIso : diff --git a/mathlib4/Mathlib/CategoryTheory/Monoidal/Comon_.lean b/mathlib4/Mathlib/CategoryTheory/Monoidal/Comon_.lean index 6a88e04c7..445f83e39 100644 --- a/mathlib4/Mathlib/CategoryTheory/Monoidal/Comon_.lean +++ b/mathlib4/Mathlib/CategoryTheory/Monoidal/Comon_.lean @@ -267,6 +267,7 @@ Turn a comonoid object into a monoid object in the opposite category. set_option backward.defeqAttrib.useBackward true in variable (C) in +set_option dsimp.resynthInstances false in /-- The contravariant functor turning comonoid objects into monoid objects in the opposite category. -/ @@ -298,6 +299,7 @@ Turn a monoid object in the opposite category into a comonoid object. variable (C) set_option backward.defeqAttrib.useBackward true in +set_option dsimp.resynthInstances false in /-- The contravariant functor turning monoid objects in the opposite category into comonoid objects. -/ diff --git a/mathlib4/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean b/mathlib4/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean index 316d26828..38ae9a9d2 100644 --- a/mathlib4/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean +++ b/mathlib4/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean @@ -242,6 +242,7 @@ instance (E : Type*) [Category* E] [MonoidalCategory E] (e : C ≌ D) : set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in instance (E : Type*) [Category* E] [MonoidalCategory E] (e : C ≌ D) : (e.congrLeft (E := E)).IsMonoidal where leftAdjoint_μ X Y := by diff --git a/mathlib4/Mathlib/CategoryTheory/Monoidal/Grp.lean b/mathlib4/Mathlib/CategoryTheory/Monoidal/Grp.lean index 9b77b6039..a4aefc6a2 100644 --- a/mathlib4/Mathlib/CategoryTheory/Monoidal/Grp.lean +++ b/mathlib4/Mathlib/CategoryTheory/Monoidal/Grp.lean @@ -674,6 +674,7 @@ def mapGrpNatTrans (f : F ⟶ F') : F.mapGrp ⟶ F'.mapGrp where set_option backward.isDefEq.respectTransparency.types false in set_option backward.defeqAttrib.useBackward true in +set_option dsimp.resynthInstances false in /-- Natural isomorphisms between functors lift to group objects. -/ @[to_additive (attr := simps!) /-- Natural isomorphisms between functors lift to additive group objects. -/] @@ -683,6 +684,7 @@ def mapGrpNatIso (e : F ≅ F') : F.mapGrp ≅ F'.mapGrp := set_option backward.isDefEq.respectTransparency.types false in set_option backward.defeqAttrib.useBackward true in attribute [local instance] Monoidal.ofChosenFiniteProducts in +set_option dsimp.resynthInstances false in /-- `mapGrp` is functorial in the left-exact functor. -/ @[to_additive (attr := simps) /-- `mapAddGrp` is functorial in the left-exact functor. -/] diff --git a/mathlib4/Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean b/mathlib4/Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean index 34136259b..f5de441ba 100644 --- a/mathlib4/Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean +++ b/mathlib4/Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean @@ -96,6 +96,7 @@ def inverseObj (F : C ⥤ Mon D) : Mon (C ⥤ D) where { one := { app X := η[(F.obj X).X] } mul := { app X := μ[(F.obj X).X] } } +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in /-- Functor translating a functor into the category of monoid objects to a monoid object in the functor category @@ -197,6 +198,7 @@ def inverseObj (F : C ⥤ Comon D) : Comon (C ⥤ D) where { counit := { app X := ε[(F.obj X).X] } comul := { app X := Δ[(F.obj X).X] } } +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.privateInPublic true in /-- Functor translating a functor into the category of comonoid objects diff --git a/mathlib4/Mathlib/CategoryTheory/Monoidal/Mon.lean b/mathlib4/Mathlib/CategoryTheory/Monoidal/Mon.lean index 09f59b9bf..22718fb73 100644 --- a/mathlib4/Mathlib/CategoryTheory/Monoidal/Mon.lean +++ b/mathlib4/Mathlib/CategoryTheory/Monoidal/Mon.lean @@ -902,6 +902,7 @@ protected instance Faithful.mapMon [F.Faithful] : F.mapMon.Faithful where map_injective {_X _Y} _f _g hfg := Mon.Hom.ext <| map_injective congr(($hfg).hom) set_option backward.defeqAttrib.useBackward true in +set_option dsimp.resynthInstances false in /-- Natural transformations between functors lift to monoid objects. -/ @[to_additive (attr := simps!) /-- Natural transformations between functors lift to additive monoid objects. -/] @@ -910,6 +911,7 @@ def mapMonNatTrans (f : F ⟶ F') [NatTrans.IsMonoidal f] : F.mapMon ⟶ F'.mapM set_option backward.isDefEq.respectTransparency.types false in set_option backward.defeqAttrib.useBackward true in +set_option dsimp.resynthInstances false in /-- Natural isomorphisms between functors lift to monoid objects. -/ @[to_additive (attr := simps!) /-- Natural isomorphisms between functors lift to additive monoid objects. -/] @@ -944,6 +946,7 @@ variable [F.Monoidal] open scoped Obj set_option backward.defeqAttrib.useBackward true in +set_option dsimp.resynthInstances false in @[to_additive] protected instance Full.mapMon [F.Full] [F.Faithful] : F.mapMon.Full where map_surjective {X Y} f := @@ -1048,6 +1051,7 @@ instance [F.Braided] : F.mapMon.Braided where set_option backward.defeqAttrib.useBackward true in variable (C D) in +set_option dsimp.resynthInstances false in /-- `mapMon` is functorial in the lax monoidal functor. -/ @[to_additive (attr := simps) /-- `mapAddMon` is functorial in the lax monoidal functor. -/] @@ -1064,6 +1068,7 @@ namespace Adjunction variable {F : C ⥤ D} {G : D ⥤ C} (a : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [a.IsMonoidal] set_option backward.defeqAttrib.useBackward true in +set_option dsimp.resynthInstances false in /-- An adjunction of monoidal functors lifts to an adjunction of their lifts to monoid objects. -/ @[to_additive (attr := simps) /-- An adjunction of monoidal functors lifts to an adjunction of their lifts to additive @@ -1125,6 +1130,7 @@ variable (C) set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Implementation of `Mon.equivLaxMonoidalFunctorPUnit`. -/ @[to_additive (attr := simps) addMonToLaxMonoidal /-- Implementation of `AddMon.equivLaxMonoidalFunctorPUnit`. -/] @@ -1139,6 +1145,7 @@ attribute [local aesop safe tactic (rule_sets := [CategoryTheory])] set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Implementation of `Mon.equivLaxMonoidalFunctorPUnit`. -/ @[to_additive (attr := simps!) /-- Implementation of `AddMon.equivLaxMonoidalFunctorPUnit`. -/] @@ -1149,6 +1156,7 @@ def unitIso : #adaptation_note /-- `respectTransparency.types true` changes the auto-generated lemmas' signature -/ +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency.types false in /-- Auxiliary definition for `counitIso`. -/ @[to_additive (attr := simps!) /-- Auxiliary definition for `counitIso`. -/] @@ -1168,12 +1176,14 @@ theorem monToLaxMonoidal_laxMonoidalToMon_obj_mul (F : Mon C) : set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in @[to_additive] theorem isMonHom_counitIsoAux (F : Mon C) : IsMonHom (counitIsoAux C F).hom where set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Implementation of `Mon.equivLaxMonoidalFunctorPUnit`. -/ @[to_additive (attr := simps!) /-- Implementation of `AddMon.equivLaxMonoidalFunctorPUnit`. -/] diff --git a/mathlib4/Mathlib/CategoryTheory/Preadditive/Mat.lean b/mathlib4/Mathlib/CategoryTheory/Preadditive/Mat.lean index 5b7a05dc3..ba12ac5ea 100644 --- a/mathlib4/Mathlib/CategoryTheory/Preadditive/Mat.lean +++ b/mathlib4/Mathlib/CategoryTheory/Preadditive/Mat.lean @@ -311,6 +311,7 @@ variable {C} set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in open scoped Classical in /-- Every object in `Mat_ C` is isomorphic to the biproduct of its summands. -/ diff --git a/mathlib4/Mathlib/CategoryTheory/ShrinkYoneda.lean b/mathlib4/Mathlib/CategoryTheory/ShrinkYoneda.lean index d5ecf21dd..1da96080b 100644 --- a/mathlib4/Mathlib/CategoryTheory/ShrinkYoneda.lean +++ b/mathlib4/Mathlib/CategoryTheory/ShrinkYoneda.lean @@ -420,6 +420,7 @@ noncomputable def uliftYonedaIsoShrinkCoyoneda : exact (shrinkCoyoneda_map_app_shrinkCoyonedaObjObjEquiv_symm _ _).symm) set_option backward.defeqAttrib.useBackward true in +set_option dsimp.resynthInstances false in /-- The functor `shrinkCoyoneda.{w}` followed by the evaluation at `Y : C` and `uliftFunctor.{v}` identifies to `yoneda.obj Y` followed by `uliftFunctor.{w}`. -/ diff --git a/mathlib4/Mathlib/CategoryTheory/SingleObj.lean b/mathlib4/Mathlib/CategoryTheory/SingleObj.lean index 780ac46e9..8d21c8adb 100644 --- a/mathlib4/Mathlib/CategoryTheory/SingleObj.lean +++ b/mathlib4/Mathlib/CategoryTheory/SingleObj.lean @@ -246,6 +246,7 @@ instance toCat_full : toCat.Full where let ⟨x, h⟩ := (SingleObj.mapHom _ _).surjective y.toFunctor ⟨ofHom x, Cat.Hom.ext h⟩ +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in instance toCat_faithful : toCat.Faithful where map_injective h := MonCat.hom_ext <| by simpa [toCat] using congr(($h).toFunctor) diff --git a/mathlib4/Mathlib/CategoryTheory/Sites/Coherent/LocallySurjective.lean b/mathlib4/Mathlib/CategoryTheory/Sites/Coherent/LocallySurjective.lean index ee9361883..007416928 100644 --- a/mathlib4/Mathlib/CategoryTheory/Sites/Coherent/LocallySurjective.lean +++ b/mathlib4/Mathlib/CategoryTheory/Sites/Coherent/LocallySurjective.lean @@ -105,6 +105,7 @@ lemma extensiveTopology.isLocallySurjective_iff [FinitaryExtensive C] set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in lemma regularTopology.isLocallySurjective_sheaf_of_types [Preregular C] [FinitaryPreExtensive C] {F G : Cᵒᵖ ⥤ Type w} (f : F ⟶ G) [PreservesFiniteProducts F] [PreservesFiniteProducts G] (h : Presheaf.IsLocallySurjective (coherentTopology C) f) : diff --git a/mathlib4/Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean b/mathlib4/Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean index 45cebad46..c5aca0c77 100644 --- a/mathlib4/Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean +++ b/mathlib4/Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean @@ -147,6 +147,7 @@ def mk {X : C} {P : Cᵒᵖ ⥤ D} {S : J.Cover X} (x : Meq P S) : ToType ((J.pl set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in theorem res_mk_eq_mk_pullback {Y X : C} {P : Cᵒᵖ ⥤ D} {S : J.Cover X} (x : Meq P S) (f : Y ⟶ X) : (J.plusObj P).map f.op (mk x) = mk (x.pullback f) := by dsimp [mk, plusObj] @@ -163,6 +164,7 @@ theorem res_mk_eq_mk_pullback {Y X : C} {P : Cᵒᵖ ⥤ D} {S : J.Cover X} (x : cases i; rfl set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in theorem toPlus_mk {X : C} {P : Cᵒᵖ ⥤ D} (S : J.Cover X) (x : ToType (P.obj (op X))) : (J.toPlus P).app _ x = mk (Meq.mk S x) := by dsimp [mk, toPlus] @@ -180,6 +182,7 @@ theorem toPlus_mk {X : C} {P : Cᵒᵖ ⥤ D} (S : J.Cover X) (x : ToType (P.obj set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in theorem toPlus_apply {X : C} {P : Cᵒᵖ ⥤ D} (S : J.Cover X) (x : Meq P S) (I : S.Arrow) : (J.toPlus P).app _ (x I) = (J.plusObj P).map I.f.op (mk x) := by dsimp only [toPlus, plusObj] @@ -214,6 +217,7 @@ theorem exists_rep {X : C} {P : Cᵒᵖ ⥤ D} (x : ToType ((J.plusObj P).obj (o simp set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in theorem eq_mk_iff_exists {X : C} {P : Cᵒᵖ ⥤ D} {S T : J.Cover X} (x : Meq P S) (y : Meq P T) : mk x = mk y ↔ ∃ (W : J.Cover X) (h1 : W ⟶ S) (h2 : W ⟶ T), x.refine h1 = y.refine h2 := by constructor diff --git a/mathlib4/Mathlib/CategoryTheory/Sites/Hypercover/Saturate.lean b/mathlib4/Mathlib/CategoryTheory/Sites/Hypercover/Saturate.lean index f2537e58f..af17fda03 100644 --- a/mathlib4/Mathlib/CategoryTheory/Sites/Hypercover/Saturate.lean +++ b/mathlib4/Mathlib/CategoryTheory/Sites/Hypercover/Saturate.lean @@ -112,6 +112,7 @@ variable {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] set_option backward.isDefEq.respectTransparency.types false in set_option backward.defeqAttrib.useBackward true in +set_option dsimp.resynthInstances false in @[simp] lemma toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks : E.toSaturateOfHasPullbacks.comp E.fromSaturateOfHasPullbacks = .id _ := by diff --git a/mathlib4/Mathlib/CategoryTheory/Sites/Monoidal.lean b/mathlib4/Mathlib/CategoryTheory/Sites/Monoidal.lean index 64b111b39..58e937447 100644 --- a/mathlib4/Mathlib/CategoryTheory/Sites/Monoidal.lean +++ b/mathlib4/Mathlib/CategoryTheory/Sites/Monoidal.lean @@ -45,6 +45,7 @@ namespace Presheaf variable [MonoidalClosed A] +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- Relation between `functorEnrichedHom` and `presheafHom`. -/ diff --git a/mathlib4/Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean b/mathlib4/Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean index 334496d1c..cb61749a3 100644 --- a/mathlib4/Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean +++ b/mathlib4/Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean @@ -219,6 +219,7 @@ lemma complete_distinguished_triangle_morphism₂ (T₁ T₂ : Triangle C) simp only [shiftEquiv'_counitIso, shift_neg_shift', assoc, Iso.inv_hom_id_app_assoc] set_option backward.defeqAttrib.useBackward true in +set_option dsimp.resynthInstances false in /-- Obvious triangles `0 ⟶ X ⟶ X ⟶ 0⟦1⟧` are distinguished -/ lemma contractible_distinguished₁ (X : C) : Triangle.mk (0 : 0 ⟶ X) (𝟙 X) 0 ∈ distTriang C := by diff --git a/mathlib4/Mathlib/Combinatorics/Enumerative/Composition.lean b/mathlib4/Mathlib/Combinatorics/Enumerative/Composition.lean index e10420920..fc31b7a78 100644 --- a/mathlib4/Mathlib/Combinatorics/Enumerative/Composition.lean +++ b/mathlib4/Mathlib/Combinatorics/Enumerative/Composition.lean @@ -813,6 +813,7 @@ Combinatorial viewpoints on compositions, seen as finite subsets of `Fin (n+1)` set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Bijection between compositions of `n` and subsets of `{0, ..., n-2}`, defined by considering the restriction of the subset to `{1, ..., n-1}` and shifting to the left by one. -/ def compositionAsSetEquiv (n : ℕ) : CompositionAsSet n ≃ Finset (Fin (n - 1)) where diff --git a/mathlib4/Mathlib/Combinatorics/Enumerative/DyckWord.lean b/mathlib4/Mathlib/Combinatorics/Enumerative/DyckWord.lean index c0c70cab5..717ad1cd0 100644 --- a/mathlib4/Mathlib/Combinatorics/Enumerative/DyckWord.lean +++ b/mathlib4/Mathlib/Combinatorics/Enumerative/DyckWord.lean @@ -308,6 +308,7 @@ lemma firstReturn_add : (p + q).firstReturn = if p = 0 then q.firstReturn else p · rw [length_range, u, length_append] exact Nat.lt_add_right _ (firstReturn_lt_length h) +set_option dsimp.resynthInstances false in @[simp] lemma firstReturn_nest : p.nest.firstReturn = p.toList.length + 1 := by have u : p.nest.toList = U :: p.toList ++ [D] := rfl diff --git a/mathlib4/Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean b/mathlib4/Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean index 57b0592ee..d97877643 100644 --- a/mathlib4/Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean +++ b/mathlib4/Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean @@ -112,6 +112,7 @@ theorem Coloring.mem_colorClasses {v : V} : C.colorClass (C v) ∈ C.colorClasse theorem Coloring.colorClasses_finite [Finite α] : C.colorClasses.Finite := Setoid.finite_classes_ker _ +set_option dsimp.resynthInstances false in theorem Coloring.card_colorClasses_le [Fintype α] [Fintype C.colorClasses] : Fintype.card C.colorClasses ≤ Fintype.card α := by simp only [colorClasses] diff --git a/mathlib4/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean b/mathlib4/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean index 335b84b79..e656d248f 100644 --- a/mathlib4/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean +++ b/mathlib4/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean @@ -90,6 +90,7 @@ theorem IsSRGWith.top : of_adj _ _ := card_commonNeighbors_top of_not_adj v w h h' := (h' ((top_adj v w).2 h)).elim +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency.types false in theorem IsSRGWith.card_neighborFinset_union_eq {v w : V} (h : G.IsSRGWith n k ℓ μ) : #(G.neighborFinset v ∪ G.neighborFinset w) = diff --git a/mathlib4/Mathlib/Condensed/Discrete/Colimit.lean b/mathlib4/Mathlib/Condensed/Discrete/Colimit.lean index 33120a7e1..fe63d66b1 100644 --- a/mathlib4/Mathlib/Condensed/Discrete/Colimit.lean +++ b/mathlib4/Mathlib/Condensed/Discrete/Colimit.lean @@ -279,6 +279,7 @@ def isoLocallyConstantOfIsColimit lanPresheafExt (isoFinYoneda F ≪≫ (locallyConstantIsoFinYoneda F).symm) ≪≫ lanPresheafNatIso fun _ ↦ isColimitLocallyConstantPresheafDiagram _ _ +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma isoLocallyConstantOfIsColimit_inv (X : Profinite.{u}ᵒᵖ ⥤ Type (u + 1)) @@ -571,6 +572,7 @@ def isoLocallyConstantOfIsColimit (hF : ∀ S : LightProfinite, IsColimit <| lanPresheafExt (isoFinYoneda F ≪≫ (locallyConstantIsoFinYoneda F).symm) ≪≫ lanPresheafNatIso fun _ ↦ isColimitLocallyConstantPresheafDiagram _ _ +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma isoLocallyConstantOfIsColimit_inv (X : LightProfinite.{u}ᵒᵖ ⥤ Type u) diff --git a/mathlib4/Mathlib/Condensed/Light/TopCatAdjunction.lean b/mathlib4/Mathlib/Condensed/Light/TopCatAdjunction.lean index e17767568..c4cff4755 100644 --- a/mathlib4/Mathlib/Condensed/Light/TopCatAdjunction.lean +++ b/mathlib4/Mathlib/Condensed/Light/TopCatAdjunction.lean @@ -120,6 +120,7 @@ noncomputable def topCatAdjunctionUnit (X : LightCondSet.{u}) : X ⟶ X.toTopCat TopCat.toSheafCompHausLike_obj_map, ← Functor.map_comp_apply] rfl } +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The adjunction `lightCondSetToTopCat ⊣ topCatToLightCondSet` -/ diff --git a/mathlib4/Mathlib/Condensed/TopCatAdjunction.lean b/mathlib4/Mathlib/Condensed/TopCatAdjunction.lean index 1fff0143b..2a938e898 100644 --- a/mathlib4/Mathlib/Condensed/TopCatAdjunction.lean +++ b/mathlib4/Mathlib/Condensed/TopCatAdjunction.lean @@ -123,6 +123,7 @@ noncomputable def topCatAdjunctionUnit (X : CondensedSet.{u}) : X ⟶ X.toTopCat TypeCat.Fun.coe_mk, ← Functor.map_comp_apply] rfl } +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The adjunction `condensedSetToTopCat ⊣ topCatToCondensedSet` -/ diff --git a/mathlib4/Mathlib/Data/DFinsupp/WellFounded.lean b/mathlib4/Mathlib/Data/DFinsupp/WellFounded.lean index a4aa314cd..d8dbf9b41 100644 --- a/mathlib4/Mathlib/Data/DFinsupp/WellFounded.lean +++ b/mathlib4/Mathlib/Data/DFinsupp/WellFounded.lean @@ -60,6 +60,7 @@ section Zero variable [∀ i, Zero (α i)] (r : ι → ι → Prop) (s : ∀ i, α i → α i → Prop) +set_option dsimp.resynthInstances false in /-- This key lemma says that if a finitely supported dependent function `x₀` is obtained by merging two such functions `x₁` and `x₂`, and if we evolve `x₀` down the `DFinsupp.Lex` relation one step and get `x`, we can always evolve one of `x₁` and `x₂` down the `DFinsupp.Lex` relation diff --git a/mathlib4/Mathlib/Data/List/MinMax.lean b/mathlib4/Mathlib/Data/List/MinMax.lean index d38bd9f57..9d46d82e9 100644 --- a/mathlib4/Mathlib/Data/List/MinMax.lean +++ b/mathlib4/Mathlib/Data/List/MinMax.lean @@ -239,6 +239,7 @@ section LinearOrder variable [LinearOrder α] {l : List α} {a m : α} +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in @[to_dual] theorem maximum_concat (a : α) (l : List α) : maximum (l ++ [a]) = max (maximum l) a := by diff --git a/mathlib4/Mathlib/Data/Matrix/PEquiv.lean b/mathlib4/Mathlib/Data/Matrix/PEquiv.lean index 7ccbc4705..8d9fe1ee5 100644 --- a/mathlib4/Mathlib/Data/Matrix/PEquiv.lean +++ b/mathlib4/Mathlib/Data/Matrix/PEquiv.lean @@ -157,6 +157,7 @@ theorem toMatrix_injective [DecidableEq n] [MulZeroOneClass α] [Nontrivial α] simp [hf.symm, Ne.symm hi] set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in theorem toMatrix_swap [DecidableEq n] [AddGroupWithOne α] (i j : n) : (Equiv.swap i j).toPEquiv.toMatrix = (1 : Matrix n n α) - (single i i).toMatrix - (single j j).toMatrix + (single i j).toMatrix + diff --git a/mathlib4/Mathlib/Data/Ordmap/Invariants.lean b/mathlib4/Mathlib/Data/Ordmap/Invariants.lean index f9b77f459..e679cfe93 100644 --- a/mathlib4/Mathlib/Data/Ordmap/Invariants.lean +++ b/mathlib4/Mathlib/Data/Ordmap/Invariants.lean @@ -554,6 +554,7 @@ theorem dual_insert [LE α] [@Std.Total α (· ≤ ·)] [DecidableLE α] (x : α set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in theorem balance_eq_balance' {l x r} (hl : Balanced l) (hr : Balanced r) (sl : Sized l) (sr : Sized r) : @balance α l x r = balance' l x r := by obtain - | ⟨ls, ll, lx, lr⟩ := l diff --git a/mathlib4/Mathlib/Data/Rat/Lemmas.lean b/mathlib4/Mathlib/Data/Rat/Lemmas.lean index e028869fc..5658e990d 100644 --- a/mathlib4/Mathlib/Data/Rat/Lemmas.lean +++ b/mathlib4/Mathlib/Data/Rat/Lemmas.lean @@ -285,6 +285,7 @@ theorem inv_intCast_num_of_pos {a : ℤ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1 theorem inv_natCast_num_of_pos {a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1 := inv_intCast_num_of_pos (mod_cast ha0 : 0 < (a : ℤ)) +set_option dsimp.resynthInstances false in theorem inv_intCast_den_of_pos {a : ℤ} (ha0 : 0 < a) : ((a : ℚ)⁻¹.den : ℤ) = a := by simp only [den_inv, num_intCast] grind diff --git a/mathlib4/Mathlib/Data/String/Basic.lean b/mathlib4/Mathlib/Data/String/Basic.lean index 8bbde03ec..0d7d3a8d3 100644 --- a/mathlib4/Mathlib/Data/String/Basic.lean +++ b/mathlib4/Mathlib/Data/String/Basic.lean @@ -53,6 +53,7 @@ def ltb (s₁ s₂ : Legacy.Iterator) : Bool := else base₁ it₁.s it₂.s it₁.i it₂.i h₂ h₁ else base₂ it₁.s it₂.s it₁.i it₂.i h₂ +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in theorem ltb_cons_addChar' (c : Char) (s₁ s₂ : Legacy.Iterator) : ltb ⟨ofList (c :: s₁.s.toList), s₁.i + c⟩ ⟨ofList (c :: s₂.s.toList), s₂.i + c⟩ = diff --git a/mathlib4/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean b/mathlib4/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean index 9a7fffe7d..ade6a9ea5 100644 --- a/mathlib4/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean +++ b/mathlib4/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean @@ -166,6 +166,7 @@ instance instField : Field (AlgebraicClosure k) where ext; simp [MvPolynomial.algebraMap_eq, Rat.smul_def] set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in theorem Monics.map_eq_prod {f : Monics k} : f.1.map (algebraMap k (AlgebraicClosure k)) = ∏ i, map (Ideal.Quotient.mk <| maxIdeal k) (X - C (MvPolynomial.X ⟨f, i⟩)) := by diff --git a/mathlib4/Mathlib/Geometry/Euclidean/Incenter.lean b/mathlib4/Mathlib/Geometry/Euclidean/Incenter.lean index 1d7b5902c..a26565450 100644 --- a/mathlib4/Mathlib/Geometry/Euclidean/Incenter.lean +++ b/mathlib4/Mathlib/Geometry/Euclidean/Incenter.lean @@ -177,6 +177,7 @@ lemma ExcenterExists.excenterWeights_ne_zero {signs : Finset (Fin (n + 1))} s.ExcenterExists signsᶜ ↔ s.ExcenterExists signs := by simp [ExcenterExists] +set_option dsimp.resynthInstances false in lemma sum_excenterWeights (signs : Finset (Fin (n + 1))) [Decidable (s.ExcenterExists signs)] : ∑ i, s.excenterWeights signs i = if s.ExcenterExists signs then 1 else 0 := by simp_rw [ExcenterExists, excenterWeights] diff --git a/mathlib4/Mathlib/Geometry/Manifold/Riemannian/Basic.lean b/mathlib4/Mathlib/Geometry/Manifold/Riemannian/Basic.lean index 7756ee06d..b19298df5 100644 --- a/mathlib4/Mathlib/Geometry/Manifold/Riemannian/Basic.lean +++ b/mathlib4/Mathlib/Geometry/Manifold/Riemannian/Basic.lean @@ -96,6 +96,7 @@ two points is the infimum of the length of paths between these points. variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F] +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in variable (F) in /-- The standard Riemannian metric on a vector space with an inner product, given by this inner diff --git a/mathlib4/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean b/mathlib4/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean index 0a3c44c17..5c1e058d0 100644 --- a/mathlib4/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean +++ b/mathlib4/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean @@ -83,6 +83,7 @@ noncomputable def coproductCofan : Cocone F where naturality := fun ⟨j⟩ ⟨j'⟩ ⟨(f : j = j')⟩ => by subst f; simp } set_option backward.defeqAttrib.useBackward true in +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in /-- The explicit coproduct cofan constructed in `coproductCofan` is indeed a colimit. -/ noncomputable def coproductCofanIsColimit : IsColimit (coproductCofan F) where diff --git a/mathlib4/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/mathlib4/Mathlib/Geometry/RingedSpace/OpenImmersion.lean index 4840c3b01..681ca7122 100644 --- a/mathlib4/Mathlib/Geometry/RingedSpace/OpenImmersion.lean +++ b/mathlib4/Mathlib/Geometry/RingedSpace/OpenImmersion.lean @@ -303,6 +303,7 @@ noncomputable section Pullback variable {X Y Z : PresheafedSpace C} (f : X ⟶ Z) [hf : IsOpenImmersion f] (g : Y ⟶ Z) +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- (Implementation.) The projection map when constructing the pullback along an open immersion. diff --git a/mathlib4/Mathlib/GroupTheory/ClassEquation.lean b/mathlib4/Mathlib/GroupTheory/ClassEquation.lean index 485f6c024..403b67493 100644 --- a/mathlib4/Mathlib/GroupTheory/ClassEquation.lean +++ b/mathlib4/Mathlib/GroupTheory/ClassEquation.lean @@ -45,6 +45,7 @@ theorem Group.sum_card_conj_classes_eq_card [Finite G] : simp [← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype] set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The **class equation** for finite groups. The cardinality of a group is equal to the size of its center plus the sum of the size of all its nontrivial conjugacy classes. -/ theorem Group.nat_card_center_add_sum_card_noncenter_eq_card [Finite G] : diff --git a/mathlib4/Mathlib/GroupTheory/Exponent.lean b/mathlib4/Mathlib/GroupTheory/Exponent.lean index ed9c964ea..ce30a1ffe 100644 --- a/mathlib4/Mathlib/GroupTheory/Exponent.lean +++ b/mathlib4/Mathlib/GroupTheory/Exponent.lean @@ -86,6 +86,7 @@ theorem exponent_multiplicative {G : Type*} [AddMonoid G] : set_option backward.isDefEq.respectTransparency false in open MulOpposite in +set_option dsimp.resynthInstances false in @[to_additive (attr := simp)] theorem _root_.MulOpposite.exponent : exponent (MulOpposite G) = exponent G := by simp only [Monoid.exponent, ExponentExists] diff --git a/mathlib4/Mathlib/GroupTheory/Perm/Fin.lean b/mathlib4/Mathlib/GroupTheory/Perm/Fin.lean index 377fb0e64..978e6f1c4 100644 --- a/mathlib4/Mathlib/GroupTheory/Perm/Fin.lean +++ b/mathlib4/Mathlib/GroupTheory/Perm/Fin.lean @@ -603,6 +603,7 @@ noncomputable def decomposeFin' : Perm (Fin (n + 2)) ≃ Fin (n + 2) × Perm (Fi lemma decomposeFin'_symm (i : Fin (n + 2)) (σ : Perm (Fin (n + 1))) : decomposeFin'.symm ⟨i, σ⟩ = decomposeFin'Symm i σ := rfl +set_option dsimp.resynthInstances false in @[simp] lemma sign_decomposeFin'Symm (i : Fin (n + 2)) (σ : Perm (Fin (n + 1))) : (decomposeFin'Symm i σ).sign = (-1) ^ i.val * σ.sign := by diff --git a/mathlib4/Mathlib/GroupTheory/Perm/Sign.lean b/mathlib4/Mathlib/GroupTheory/Perm/Sign.lean index 44d53713a..c623a3d45 100644 --- a/mathlib4/Mathlib/GroupTheory/Perm/Sign.lean +++ b/mathlib4/Mathlib/GroupTheory/Perm/Sign.lean @@ -225,6 +225,7 @@ theorem signAux_inv {n : ℕ} (f : Perm (Fin n)) : signAux f⁻¹ = signAux f := · simp_all [signBijAux, (mem_finPairsLT.1 hab).not_ge] · simp_all [signBijAux, dite_eq_right h, (mem_finPairsLT.1 hab).le] +set_option dsimp.resynthInstances false in theorem signAux_mul {n : ℕ} (f g : Perm (Fin n)) : signAux (f * g) = signAux f * signAux g := by rw [← signAux_inv g] unfold signAux diff --git a/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean b/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean index bebd5b164..29d81c913 100644 --- a/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean +++ b/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean @@ -738,6 +738,7 @@ theorem reindex_symm (e : ι ≃ ι₂) : simp [reindex] set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in @[simp] theorem reindex_refl : reindex R s (Equiv.refl ι) = LinearEquiv.refl R _ := by ext diff --git a/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean b/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean index cf611204a..df0a9ac35 100644 --- a/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean +++ b/mathlib4/Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean @@ -89,6 +89,7 @@ Then both backward compatibility options can go: first `respectTransparency fals -/ set_option backward.isDefEq.respectTransparency.instanceSearchTypes false in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in @[simp] lemma equivPiTensorComplSingletonTensor_tprod (i₀ : ι) (m : ∀ i, M i) : equivPiTensorComplSingletonTensor R M i₀ (⨂ₜ[R] i, m i) = diff --git a/mathlib4/Mathlib/LinearAlgebra/Semisimple.lean b/mathlib4/Mathlib/LinearAlgebra/Semisimple.lean index 8c9f85f85..8e921253d 100644 --- a/mathlib4/Mathlib/LinearAlgebra/Semisimple.lean +++ b/mathlib4/Mathlib/LinearAlgebra/Semisimple.lean @@ -274,6 +274,7 @@ include comm hf hg set_option backward.isDefEq.respectTransparency false in attribute [local simp] Submodule.Quotient.quot_mk_eq_mk in +set_option dsimp.resynthInstances false in theorem IsSemisimple.of_mem_adjoin_pair {a : End K M} (ha : a ∈ K[f, g]) : a.IsSemisimple := by let R := K[X] ⧸ Ideal.span {minpoly K f} diff --git a/mathlib4/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean b/mathlib4/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean index 4d9efdbfb..f73cadda2 100644 --- a/mathlib4/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean +++ b/mathlib4/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean @@ -480,6 +480,7 @@ the integral ideal `J`. -/ def idealSet : Set (mixedSpace K) := fundamentalCone K ∩ (mixedEmbedding.idealLattice K (FractionalIdeal.mk0 K J)) +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency.types false in variable {K J} in theorem mem_idealSet : diff --git a/mathlib4/Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean b/mathlib4/Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean index 8f1515299..209eef5b0 100644 --- a/mathlib4/Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean +++ b/mathlib4/Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean @@ -612,6 +612,7 @@ open nonZeroDivisors IsPrimitiveRoot variable (K p k) variable [CharZero K] +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in /-- We compute the absolute discriminant of a `p ^ k`-th cyclotomic field. Beware that in the cases `p ^ k = 1` and `p ^ k = 2` the formula uses `1 / 2 = 0` and `0 - 1 = 0`. diff --git a/mathlib4/Mathlib/NumberTheory/Padics/WithVal.lean b/mathlib4/Mathlib/NumberTheory/Padics/WithVal.lean index 4223bc0b8..84e4c39d3 100644 --- a/mathlib4/Mathlib/NumberTheory/Padics/WithVal.lean +++ b/mathlib4/Mathlib/NumberTheory/Padics/WithVal.lean @@ -71,6 +71,7 @@ Potential fix: make the following definitions implicit-reducible: Then both backward compatibility options can go. -/ +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency.types false in set_option backward.isDefEq.respectTransparency.instanceSearchTypes false in open MonoidWithZeroHom.ValueGroup₀ in diff --git a/mathlib4/Mathlib/Order/Birkhoff.lean b/mathlib4/Mathlib/Order/Birkhoff.lean index 68452bd35..af3a5210e 100644 --- a/mathlib4/Mathlib/Order/Birkhoff.lean +++ b/mathlib4/Mathlib/Order/Birkhoff.lean @@ -127,6 +127,7 @@ namespace OrderIso section SemilatticeSup variable [SemilatticeSup α] [OrderBot α] [Finite α] +set_option dsimp.resynthInstances false in @[to_dual (attr := simp)] lemma supIrredLowerSet_symm_apply (s : {s : LowerSet α // SupIrred s}) [Fintype s] : supIrredLowerSet.symm s = (s.1 : Set α).toFinset.sup id := by diff --git a/mathlib4/Mathlib/Probability/ProbabilityMassFunction/Monad.lean b/mathlib4/Mathlib/Probability/ProbabilityMassFunction/Monad.lean index 8bfbf6b5d..be3a47c31 100644 --- a/mathlib4/Mathlib/Probability/ProbabilityMassFunction/Monad.lean +++ b/mathlib4/Mathlib/Probability/ProbabilityMassFunction/Monad.lean @@ -244,6 +244,7 @@ theorem bindOnSupport_pure (p : PMF α) : (p.bindOnSupport fun a _ => pure a) = simp only [PMF.bind_pure, PMF.bindOnSupport_eq_bind] set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in @[simp] theorem bindOnSupport_bindOnSupport (p : PMF α) (f : ∀ a ∈ p.support, PMF β) (g : ∀ b ∈ (p.bindOnSupport f).support, PMF γ) : diff --git a/mathlib4/Mathlib/RepresentationTheory/Homological/FiniteCyclic.lean b/mathlib4/Mathlib/RepresentationTheory/Homological/FiniteCyclic.lean index a2fa10115..b42b2eafe 100644 --- a/mathlib4/Mathlib/RepresentationTheory/Homological/FiniteCyclic.lean +++ b/mathlib4/Mathlib/RepresentationTheory/Homological/FiniteCyclic.lean @@ -205,6 +205,7 @@ noncomputable def resolution.π (g : G) : set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in lemma resolution_quasiIso (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) : QuasiIso (resolution.π k g) where quasiIsoAt m := by diff --git a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean index ecf58e38b..02f1798b4 100644 --- a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean +++ b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean @@ -98,6 +98,7 @@ def d [Monoid G] (A : Rep k G) (n : ℕ) : variable [Group G] (A : Rep k G) (n : ℕ) +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in theorem d_eq : diff --git a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/FiniteCyclic.lean b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/FiniteCyclic.lean index 74b202ee6..728402073 100644 --- a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/FiniteCyclic.lean +++ b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/FiniteCyclic.lean @@ -49,6 +49,7 @@ variable {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Given a finite cyclic group `G` generated by `g : G` and a `k`-linear `G`-representation `A`, the periodic cochain complex `0 ⟶ Hom(k[G], A) --(- ∘ (ρ(g) - 𝟙))--> Hom(k[G], A) --(- ∘ N)--> Hom(k[G], A) ⟶ ...` diff --git a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean index b58f066d9..55a4381b7 100644 --- a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean +++ b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean @@ -117,6 +117,7 @@ variable {K L} [IsGalois K L] open Additive Rep set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Given `L/K` finite and Galois, and `x : Lˣ`, this essentially says `(∏ σ) • x = N_{L/K}(x)`, where the product is over `σ ∈ Gal(L/K)`. -/ theorem norm_ofAlgebraAutOnUnits_eq (x : Lˣ) : @@ -128,6 +129,7 @@ variable [IsCyclic (L ≃ₐ[K] L)] {g : Gal(L/K)} set_option backward.isDefEq.respectTransparency false in attribute [local instance] IsCyclic.commGroup in +set_option dsimp.resynthInstances false in /-- Hilbert's Theorem 90: given a finite cyclic Galois extension `L/K`, an element `x : L` such that `N_{L/K}(x) = 1`, and a generator `g` of `Gal(L/K)`, there exists `y : Lˣ` such that `y/g y = x`. -/ diff --git a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/LongExactSequence.lean b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/LongExactSequence.lean index 174602e2e..b64e0a587 100644 --- a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/LongExactSequence.lean +++ b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/LongExactSequence.lean @@ -47,6 +47,7 @@ include hX set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in lemma map_cochainsFunctor_shortExact : ShortExact (X.map (cochainsFunctor k G)) := HomologicalComplex.shortExact_of_degreewise_shortExact _ fun i => { diff --git a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean index b6db6998c..959d3f94b 100644 --- a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean +++ b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean @@ -971,6 +971,7 @@ variable {A} set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in lemma H1π_eq_zero_iff (x : cocycles₁ A) : H1π A x = 0 ↔ ⇑x ∈ coboundaries₁ A := by have h := leftHomologyπ_naturality'_assoc (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData (leftHomologyData _) @@ -1052,6 +1053,7 @@ variable {A} set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in lemma H2π_eq_zero_iff (x : cocycles₂ A) : H2π A x = 0 ↔ ⇑x ∈ coboundaries₂ A := by have h := leftHomologyπ_naturality'_assoc (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData (leftHomologyData _) diff --git a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean index 6c7ff337e..ec64772c2 100644 --- a/mathlib4/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean +++ b/mathlib4/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean @@ -924,6 +924,7 @@ instance : Epi (H1π A) := inferInstanceAs <| Epi (_ ≫ _) variable {A} +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma H1π_eq_zero_iff (x : cycles₁ A) : H1π A x = 0 ↔ x.1 ∈ boundaries₁ A := by @@ -1006,6 +1007,7 @@ def H1ToTensorOfIsTrivial : H1 A →ₗ[ℤ] (Additive <| Abelianization G) ⊗[ set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in variable {A} in +set_option dsimp.resynthInstances false in @[simp] lemma H1ToTensorOfIsTrivial_H1π_single (g : G) (a : A) : H1ToTensorOfIsTrivial A (H1π A <| (cycles₁IsoOfIsTrivial A).inv (single g a)) = @@ -1071,6 +1073,7 @@ instance : Epi (H2π A) := inferInstanceAs <| Epi (_ ≫ _) variable {A} +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma H2π_eq_zero_iff (x : cycles₂ A) : H2π A x = 0 ↔ x.1 ∈ boundaries₂ A := by diff --git a/mathlib4/Mathlib/RepresentationTheory/Homological/Resolution.lean b/mathlib4/Mathlib/RepresentationTheory/Homological/Resolution.lean index 88756a3bd..9f6130223 100644 --- a/mathlib4/Mathlib/RepresentationTheory/Homological/Resolution.lean +++ b/mathlib4/Mathlib/RepresentationTheory/Homological/Resolution.lean @@ -209,6 +209,7 @@ instance x_projective (G : Type u) [Group G] (n : ℕ) : set_option backward.defeqAttrib.useBackward true in unif_hint where ⊢ Action.V (Action.ofMulAction G (Fin (n + 1) → G)) ≟ Fin (n + 1) → G in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Simpler expression for the differential in the standard resolution of `k` as a `G`-representation. It sends `(g₀, ..., gₙ₊₁) ↦ ∑ (-1)ⁱ • (g₀, ..., ĝᵢ, ..., gₙ₊₁)`. -/ theorem d_eq (n : ℕ) : ((standardComplex k G).d (n + 1) n).hom.toLinearMap = @@ -264,6 +265,7 @@ def ε : Rep.ofMulAction k G (Fin 1 → G) ⟶ Rep.trivial k G k := ofHom set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The homotopy equivalence of complexes of `k`-modules between the standard resolution of `k` as a trivial `G`-representation, and the complex which is `k` at 0 and 0 everywhere else, acts as `∑ nᵢgᵢ ↦ ∑ nᵢ : k[G¹] → k` at 0. -/ diff --git a/mathlib4/Mathlib/RepresentationTheory/Rep/Basic.lean b/mathlib4/Mathlib/RepresentationTheory/Rep/Basic.lean index 49b945d3a..1e64a614f 100644 --- a/mathlib4/Mathlib/RepresentationTheory/Rep/Basic.lean +++ b/mathlib4/Mathlib/RepresentationTheory/Rep/Basic.lean @@ -769,6 +769,7 @@ protected noncomputable def ihom : Rep k G ⥤ Rep k G where set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- Given a `k`-linear `G`-representation `A`, this is the Hom-set bijection in the adjunction `A ⊗ - ⊣ ihom(A, -)`. It sends `f : A ⊗ B ⟶ C` to a `Rep k G` morphism defined by currying the `k`-linear map underlying `f`, giving a map `A →ₗ[k] B →ₗ[k] C`, then flipping the arguments. -/ diff --git a/mathlib4/Mathlib/RepresentationTheory/Rep/Iso.lean b/mathlib4/Mathlib/RepresentationTheory/Rep/Iso.lean index 9ebaec5da..e27a0e41a 100644 --- a/mathlib4/Mathlib/RepresentationTheory/Rep/Iso.lean +++ b/mathlib4/Mathlib/RepresentationTheory/Rep/Iso.lean @@ -115,6 +115,7 @@ theorem ofModuleMonoidAlgebra_obj_ρ (M : ModuleCat.{w} k[G]) : (ofModuleMonoidAlgebra.obj M).ρ = Representation.ofModule M := rfl +set_option dsimp.resynthInstances false in /-- Auxiliary definition for `equivalenceModuleMonoidAlgebra`. -/ def counitIsoAddEquiv {M : ModuleCat.{w} k[G]} : (ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M ≃+ M := by @@ -122,6 +123,7 @@ def counitIsoAddEquiv {M : ModuleCat.{w} k[G]} : exact (Representation.ofModule M).asModuleEquiv.toAddEquiv.trans (RestrictScalars.addEquiv k k[G] _) +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in /-- Auxiliary definition for `equivalenceModuleMonoidAlgebra`. -/ def unitIsoAddEquiv {V : Rep.{w} k G} : V ≃+ (toModuleMonoidAlgebra ⋙ @@ -138,6 +140,7 @@ def counitIso (M : ModuleCat.{w} k[G]) : map_smul' := fun r x => by simp [counitIsoAddEquiv] } +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in theorem unit_iso_comm (V : Rep.{w} k G) (g : G) (x : V) : diff --git a/mathlib4/Mathlib/RepresentationTheory/Tannaka.lean b/mathlib4/Mathlib/RepresentationTheory/Tannaka.lean index 87eeff7d9..0394139cf 100644 --- a/mathlib4/Mathlib/RepresentationTheory/Tannaka.lean +++ b/mathlib4/Mathlib/RepresentationTheory/Tannaka.lean @@ -197,6 +197,7 @@ def leftRegularFDRepHom (s : G) : End (rightFDRep : FDRep k G) where apply congrArg f exact mul_assoc .. +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in lemma toRightFDRepComp_in_rightRegular [IsDomain k] (η : Aut (forget k G)) : ∃ (s : G), (η.hom.hom.app rightFDRep).hom.hom = rightRegular s := by diff --git a/mathlib4/Mathlib/RingTheory/ClassGroup/Basic.lean b/mathlib4/Mathlib/RingTheory/ClassGroup/Basic.lean index d74fafaf5..befce8b5b 100644 --- a/mathlib4/Mathlib/RingTheory/ClassGroup/Basic.lean +++ b/mathlib4/Mathlib/RingTheory/ClassGroup/Basic.lean @@ -205,6 +205,7 @@ def ClassGroup.equiv : (Units.mapEquiv (FractionalIdeal.canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv) this set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in @[simp] theorem ClassGroup.equiv_mk (K' : Type*) [Field K'] [Algebra R K'] [IsFractionRing R K'] (I : (FractionalIdeal R⁰ K)ˣ) : diff --git a/mathlib4/Mathlib/RingTheory/Etale/Finite.lean b/mathlib4/Mathlib/RingTheory/Etale/Finite.lean index ee6aec3ce..076e808fe 100644 --- a/mathlib4/Mathlib/RingTheory/Etale/Finite.lean +++ b/mathlib4/Mathlib/RingTheory/Etale/Finite.lean @@ -128,6 +128,7 @@ def FiniteEtale.finiteSpec (k : Type u) [Field k] : (FiniteEtale.{v} k)ᵒᵖ map f := FintypeCat.homMk (PrimeSpectrum.comap f.unop.hom.hom) set_option backward.defeqAttrib.useBackward true in +set_option dsimp.resynthInstances false in /-- If the geometric point `Ω` factors through `S`, the fiber can be computed after base change to `S`. -/ @[expose] @@ -155,6 +156,7 @@ noncomputable def FiniteEtale.fiberIsoComp [IsSepClosed Ω] : set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- If `Ω` is a separably closed field, the category of finite étale `Ω`-algebras is anti-equivalent to `FintypeCat`. -/ @[expose, simps! functor inverse_obj inverse_map] diff --git a/mathlib4/Mathlib/RingTheory/Etale/StandardEtale.lean b/mathlib4/Mathlib/RingTheory/Etale/StandardEtale.lean index 7d328ace8..65d57b97f 100644 --- a/mathlib4/Mathlib/RingTheory/Etale/StandardEtale.lean +++ b/mathlib4/Mathlib/RingTheory/Etale/StandardEtale.lean @@ -80,6 +80,7 @@ def lift (x : S) (h : P.HasMap x) : P.Ring →ₐ[R] S := Ideal.Quotient.liftₐ _ (aevalAeval x ↑(h.2.unit⁻¹)) (Ideal.span_le (I := RingHom.ker _).mpr (by simp [Set.pair_subset_iff, h.1])) +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in @[simp] lemma lift_X (x : S) (h : P.HasMap x) : P.lift x h P.X = x := by @@ -96,6 +97,7 @@ lemma HasMap.isUnit_derivative_f {x : S} (h : P.HasMap x) : ⟨_, by simpa [h.1] using congr(aeval x $e.symm)⟩ exact isUnit_of_dvd_unit this (.pow _ h.2) +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in lemma aeval_X_g_mul_mk_X : aeval P.X P.g * Ideal.Quotient.mk _ .X = 1 := by have : aeval (R := R) P.X = (Ideal.Quotient.mkₐ _ _).comp Polynomial.CAlgHom := by @@ -105,6 +107,7 @@ lemma aeval_X_g_mul_mk_X : aeval P.X P.g * Ideal.Quotient.mk _ .X = 1 := by rw [← map_mul, ← map_one (Ideal.Quotient.mk _), ← sub_eq_zero, ← map_sub, mul_comm] exact Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span (Set.mem_insert_of_mem _ rfl)) +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in variable {P} in lemma hasMap_X : P.HasMap P.X := @@ -113,6 +116,7 @@ lemma hasMap_X : P.HasMap P.X := ⟨this ▸ Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span (Set.mem_insert _ _)), IsUnit.of_mul_eq_one _ P.aeval_X_g_mul_mk_X⟩ +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in variable {P} in @[ext] @@ -236,6 +240,7 @@ def equivMvPolynomialQuotient : Ideal.quotientEquivAlg _ _ (Bivariate.equivMvPolynomial R) (by simp [Ideal.map_span]) +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in @[simp] lemma equivMvPolynomialQuotient_symm_apply : diff --git a/mathlib4/Mathlib/RingTheory/Extension/Basic.lean b/mathlib4/Mathlib/RingTheory/Extension/Basic.lean index ef31a53ee..d447f9855 100644 --- a/mathlib4/Mathlib/RingTheory/Extension/Basic.lean +++ b/mathlib4/Mathlib/RingTheory/Extension/Basic.lean @@ -283,6 +283,7 @@ def Hom.mapKer (f : P.Hom P') set_option backward.isDefEq.respectTransparency false in attribute [local instance] Algebra.TensorProduct.rightAlgebra in +set_option dsimp.resynthInstances false in /-- The canonical hom from `P` to its base change `P.baseChange`. -/ @[simps] noncomputable def toBaseChange (T : Type*) [CommRing T] [Algebra R T] : diff --git a/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basic.lean b/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basic.lean index 42c98901b..19380a423 100644 --- a/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basic.lean +++ b/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basic.lean @@ -444,6 +444,7 @@ lemma cotangentSpaceBasis_repr_tmul (r x i) : simp only [cotangentSpaceBasis, Basis.baseChange_repr_tmul, mvPolynomialBasis_repr_apply, Algebra.smul_def, mul_comm r, algebraMap_apply, toExtension] +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma cotangentSpaceBasis_repr_one_tmul (x i) : @@ -465,6 +466,7 @@ def cotangentRestrict {σ : Type*} {u : σ → ι} (hu : Function.Injective u) : Finsupp.lcomapDomain u hu ∘ₗ P.cotangentSpaceBasis.repr.toLinearMap ∘ₗ P.toExtension.cotangentComplex +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma cotangentRestrict_mk {σ : Type*} {u : σ → ι} (hu : Function.Injective u) (x : P.ker) : @@ -499,6 +501,7 @@ lemma repr_CotangentSpaceMap (f : Hom P P') (i j) : rw [CotangentSpace.map_tmul, map_one] erw [cotangentSpaceBasis_repr_one_tmul, Hom.toAlgHom_X] +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma toKaehler_tmul_D (i) : @@ -518,6 +521,7 @@ set_option backward.isDefEq.respectTransparency false in -- TODO: generalize to essentially of finite presentation algebras open KaehlerDifferential in attribute [local instance] Module.finitePresentation_of_projective in +set_option dsimp.resynthInstances false in instance [Algebra.FinitePresentation R S] : Module.FinitePresentation S Ω[S⁄R] := by let P := Algebra.Presentation.ofFinitePresentation R S have : Algebra.FiniteType R P.toExtension.Ring := by @@ -582,6 +586,7 @@ abbrev Generators.equivH1Cotangent (P : Generators R S ι) : set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in attribute [local instance] Module.finitePresentation_of_projective in +set_option dsimp.resynthInstances false in instance [FinitePresentation R S] [Module.Projective S Ω[S⁄R]] : Module.Finite S (H1Cotangent R S) := by let P := Algebra.Presentation.ofFinitePresentation R S diff --git a/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basis.lean b/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basis.lean index 1ac4a3ab3..1093669e1 100644 --- a/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basis.lean +++ b/mathlib4/Mathlib/RingTheory/Extension/Cotangent/Basis.lean @@ -59,6 +59,7 @@ of `I/I²` in `I`. -/ abbrev T := MvPolynomial ι R ⧸ (Ideal.span <| Set.range <| Subtype.val ∘ D.f ∘ b) +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The map `R[X₁, ..., Xₙ] → S` factors via `T`, because the `bᵢ` are in `I`. -/ @@ -112,6 +113,7 @@ def presLeft : Presentation R D.T ι σ := def kerGen (i : σ) : D.presLeft.toExtension.ker := ⟨(D.f (b i)).val, Presentation.mem_ker_naive _ _ i⟩ +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- The identity on `R[X₁, ..., Xₙ]` as a map of presentations of `T` to `S`. -/ @@ -124,6 +126,7 @@ lemma toAlgHom_fhom : D.fhom.toAlgHom = AlgHom.id R P.Ring := by ext : 1 simp [fhom] +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma ker_presLeft_le : D.presLeft.ker ≤ P.ker := by @@ -137,6 +140,7 @@ set_option backward.isDefEq.respectTransparency.types false in def tensorCotangentHom : S ⊗[D.T] D.presLeft.toExtension.Cotangent →ₗ[S] P.toExtension.Cotangent := LinearMap.liftBaseChange _ (Extension.Cotangent.map D.fhom.toExtensionHom) +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma tensorCotangentHom_tmul (x : D.presLeft.toExtension.ker) : @@ -193,6 +197,7 @@ set_option backward.isDefEq.respectTransparency false in def pres : Presentation R S (Unit ⊕ ι) (Unit ⊕ σ) := D.presRight.comp D.presLeft +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma map_ofComp_mk [Nontrivial S] : @@ -352,6 +357,7 @@ set_option backward.isDefEq.respectTransparency.instanceSearchTypes false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in open PresentationOfFreeCotangent in +set_option dsimp.resynthInstances false in /-- Version of `Algebra.Generators.exists_presentation_of_free_cotangent` taking a basis instead of a `Module.Free` assumption. diff --git a/mathlib4/Mathlib/RingTheory/Extension/ExtendScalars.lean b/mathlib4/Mathlib/RingTheory/Extension/ExtendScalars.lean index 6a2412aac..204a24342 100644 --- a/mathlib4/Mathlib/RingTheory/Extension/ExtendScalars.lean +++ b/mathlib4/Mathlib/RingTheory/Extension/ExtendScalars.lean @@ -58,6 +58,7 @@ def extendScalars {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R set_option backward.isDefEq.respectTransparency false in set_option backward.defeqAttrib.useBackward true in +set_option dsimp.resynthInstances false in /-- The canonical homomorphism from `P` to `P.extendScalars` induced by the identity map on the underlying extension rings. -/ @[simps!] diff --git a/mathlib4/Mathlib/RingTheory/Extension/Generators.lean b/mathlib4/Mathlib/RingTheory/Extension/Generators.lean index edf96eefc..541b97a16 100644 --- a/mathlib4/Mathlib/RingTheory/Extension/Generators.lean +++ b/mathlib4/Mathlib/RingTheory/Extension/Generators.lean @@ -286,6 +286,7 @@ def baseChange (T) [CommRing T] [Algebra R T] (P : Generators R S ι) : set_option backward.defeqAttrib.useBackward true in variable (T) in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The forwards direction of the canonical isomorphism `T ⊗[R] R[Xᵢ] ≃ₐ[T] T[Xᵢ]` as a map of extensions. -/ noncomputable def baseChangeFromBaseChange : @@ -304,6 +305,7 @@ lemma baseChangeFromBaseChange_apply (x : P.toExtension.baseChange.Ring) : set_option backward.defeqAttrib.useBackward true in variable (T) in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The backwards direction of the canonical isomorphism `T ⊗[R] R[Xᵢ] ≃ₐ[T] T[Xᵢ]` as a map of extensions. -/ noncomputable def baseChangeToBaseChange : @@ -594,6 +596,7 @@ def toExtendScalars (P : Generators R T ι) : Hom P (P.extendScalars S) where set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in variable {P P'} in +set_option dsimp.resynthInstances false in /-- Reinterpret a hom between generators as a hom between extensions. -/ @[simps] noncomputable @@ -605,6 +608,7 @@ def Hom.toExtensionHom [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in @[simp] lemma Hom.toExtensionHom_id : Hom.toExtensionHom (.id P) = .id _ := by ext; simp @@ -627,6 +631,7 @@ noncomputable abbrev ker : Ideal P.Ring := P.toExtension.ker set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in lemma ker_eq_ker_aeval_val : P.ker = RingHom.ker (aeval P.val) := by simp only [ker, Extension.ker, toExtension_Ring, algebraMap_eq] rfl @@ -644,6 +649,7 @@ lemma ker_naive {σ : Type*} {I : Ideal (MvPolynomial σ R)} set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in @[simp] lemma ker_ofAlgHom {I : Type*} (f : MvPolynomial I R →ₐ[R] S) (h : Function.Surjective ⇑f) : (ofAlgHom f h).ker = RingHom.ker f.toRingHom := by @@ -802,6 +808,7 @@ namespace Algebra.Extension set_option backward.isDefEq.respectTransparency false in set_option backward.defeqAttrib.useBackward true in +set_option dsimp.resynthInstances false in /-- The canonical homomorphism of extensions from the universal extension `R[S] → S` (given by `Generators.self R S`) to any extension `P` defined via the designated section `P.σ`. -/ @[simps!] diff --git a/mathlib4/Mathlib/RingTheory/Extension/Presentation/Core.lean b/mathlib4/Mathlib/RingTheory/Extension/Presentation/Core.lean index 3e486502c..8b0648163 100644 --- a/mathlib4/Mathlib/RingTheory/Extension/Presentation/Core.lean +++ b/mathlib4/Mathlib/RingTheory/Extension/Presentation/Core.lean @@ -88,6 +88,7 @@ class HasCoeffs (R₀ : Type*) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] where coeffs_subset_range : P.coeffs ⊆ Set.range (algebraMap R₀ R) +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in instance : P.HasCoeffs P.Core where coeffs_subset_range := by @@ -245,6 +246,7 @@ namespace Algebra.SubmersivePresentation variable [Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one diff --git a/mathlib4/Mathlib/RingTheory/Kaehler/JacobiZariski.lean b/mathlib4/Mathlib/RingTheory/Kaehler/JacobiZariski.lean index 55b78cefc..112d9f982 100644 --- a/mathlib4/Mathlib/RingTheory/Kaehler/JacobiZariski.lean +++ b/mathlib4/Mathlib/RingTheory/Kaehler/JacobiZariski.lean @@ -89,6 +89,7 @@ lemma Cotangent.surjective_map_ofComp : set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in open Extension.Cotangent in +set_option dsimp.resynthInstances false in /-- Given representations `0 → I → R[X] → S → 0` and `0 → K → S[Y] → T → 0`, we may consider the induced representation `0 → J → R[X, Y] → T → 0`, and the sequence @@ -365,6 +366,7 @@ def δ : (Cotangent.surjective_map_ofComp Q P) (CotangentSpace.map_toComp_injective Q P) +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma exact_δ_map : diff --git a/mathlib4/Mathlib/RingTheory/LittleWedderburn.lean b/mathlib4/Mathlib/RingTheory/LittleWedderburn.lean index f08adb7eb..0b187e3b3 100644 --- a/mathlib4/Mathlib/RingTheory/LittleWedderburn.lean +++ b/mathlib4/Mathlib/RingTheory/LittleWedderburn.lean @@ -64,6 +64,7 @@ def field (hD : InductionHyp D) {R : Subring D} (hR : R < ⊤) mul_comm := fun x y ↦ Subtype.ext <| hD hR x.2 y.2 } set_option backward.isDefEq.respectTransparency.types false in +set_option dsimp.resynthInstances false in /-- We prove that if every subring of `D` is central, then so is `D`. -/ theorem center_eq_top [Finite D] (hD : InductionHyp D) : Subring.center D = ⊤ := by classical diff --git a/mathlib4/Mathlib/RingTheory/LocalProperties/InjectiveDimension.lean b/mathlib4/Mathlib/RingTheory/LocalProperties/InjectiveDimension.lean index 31012cc24..3ecd260f6 100644 --- a/mathlib4/Mathlib/RingTheory/LocalProperties/InjectiveDimension.lean +++ b/mathlib4/Mathlib/RingTheory/LocalProperties/InjectiveDimension.lean @@ -30,6 +30,7 @@ variable {R : Type u} [CommRing R] open CategoryTheory Limits +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in instance [Small.{v} R] [IsNoetherianRing R] (S : Submonoid R) : (ModuleCat.localizedModuleFunctor.{v} S).PreservesInjectiveObjects where diff --git a/mathlib4/Mathlib/RingTheory/LocalProperties/ProjectiveDimension.lean b/mathlib4/Mathlib/RingTheory/LocalProperties/ProjectiveDimension.lean index 01688ee04..f1b05e381 100644 --- a/mathlib4/Mathlib/RingTheory/LocalProperties/ProjectiveDimension.lean +++ b/mathlib4/Mathlib/RingTheory/LocalProperties/ProjectiveDimension.lean @@ -30,6 +30,7 @@ namespace ModuleCat open CategoryTheory +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in instance [Small.{v} R] (S : Submonoid R) : (ModuleCat.localizedModuleFunctor.{v} S).PreservesProjectiveObjects where diff --git a/mathlib4/Mathlib/RingTheory/Morita/Matrix.lean b/mathlib4/Mathlib/RingTheory/Morita/Matrix.lean index fbd380664..a753f8b5e 100644 --- a/mathlib4/Mathlib/RingTheory/Morita/Matrix.lean +++ b/mathlib4/Mathlib/RingTheory/Morita/Matrix.lean @@ -131,6 +131,7 @@ def fromModuleCatToModuleCatLinearEquiv (M : Type*) [AddCommGroup M] [Module R M right_inv x := by simp set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The natural isomorphism showing that `toModuleCat` is the left inverse of `toMatrixModCat`. -/ def MatrixModCat.unitIso (i : ι) : ModuleCat.toMatrixModCat R ι ⋙ MatrixModCat.toModuleCat R i ≅ 𝟭 (ModuleCat R) := @@ -171,6 +172,7 @@ def toModuleCatFromModuleCatLinearEquiv (M : ModuleCat (Matrix ι ι R)) (j : ι simp [← mul_smul, ← hy] set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The natural isomorphism showing that `toMatrixModCat` is the right inverse of `toModuleCat`. -/ def MatrixModCat.counitIso (i : ι) : MatrixModCat.toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι ≅ 𝟭 (ModuleCat (Matrix ι ι R)) := @@ -181,6 +183,7 @@ def MatrixModCat.counitIso (i : ι) : set_option backward.isDefEq.respectTransparency false in -- This declaration has been on the tipping point of timeout ever since nightly-2026-02-23. +set_option dsimp.resynthInstances false in /-- `ModuleCat.toMatrixModCat R ι` and `MatrixModCat.toModuleCat R i` together form an equivalence of categories. -/ @[simps, stacks 074D "(1)"] @@ -200,6 +203,7 @@ def ModuleCat.matrixEquivalence (i : ι) : ModuleCat R ≌ ModuleCat (Matrix ι set_option backward.isDefEq.respectTransparency false in open ModuleCat.Algebra in +set_option dsimp.resynthInstances false in /-- Moreover `ModuleCat.matrixEquivalence` is a `MoritaEquivalence`. -/ @[simps] def moritaEquivalenceMatrix (R₀ : Type*) [CommRing R₀] [Algebra R₀ R] (i : ι) : diff --git a/mathlib4/Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean b/mathlib4/Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean index 37c4fb410..9baae6ff8 100644 --- a/mathlib4/Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean +++ b/mathlib4/Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean @@ -387,11 +387,13 @@ section WeightedHomogeneousComponent variable {w : σ → M} (n : M) (φ : MvPolynomial σ R) +set_option dsimp.resynthInstances false in theorem coeff_weightedHomogeneousComponent [DecidableEq M] (d : σ →₀ ℕ) : (weightedHomogeneousComponent w n φ).coeff d = if weight w d = n then φ.coeff d else 0 := by simp [weightedHomogeneousComponent, MvPolynomial, Finsupp.filter_apply] +set_option dsimp.resynthInstances false in theorem weightedHomogeneousComponent_apply [DecidableEq M] : weightedHomogeneousComponent w n φ = ∑ d ∈ φ.support with weight w d = n, monomial d (φ.coeff d) := by diff --git a/mathlib4/Mathlib/RingTheory/Perfection.lean b/mathlib4/Mathlib/RingTheory/Perfection.lean index ac4546542..1e503ecef 100644 --- a/mathlib4/Mathlib/RingTheory/Perfection.lean +++ b/mathlib4/Mathlib/RingTheory/Perfection.lean @@ -679,12 +679,14 @@ theorem coeff_pow_p (x : PreTilt O p) (n : ℕ) : coeff (n + 1) x ^ p = coeff n Perfection.coeff_pow_p x n set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in @[simp] theorem coeff_frobeniusEquiv_symm (n : ℕ) (x : PreTilt O p) : (coeff n (((frobeniusEquiv _ p).symm) x)) = coeff (n + 1) x := by simp [PreTilt, coeff] set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in @[simp] theorem coeff_iterate_frobeniusEquiv_symm (m n : ℕ) (x : PreTilt O p) : (coeff m (((frobeniusEquiv _ p).symm^[n]) x)) = coeff (m + n) x := by diff --git a/mathlib4/Mathlib/RingTheory/Polynomial/Resultant/Basic.lean b/mathlib4/Mathlib/RingTheory/Polynomial/Resultant/Basic.lean index 5af96ec82..d3ad24788 100644 --- a/mathlib4/Mathlib/RingTheory/Polynomial/Resultant/Basic.lean +++ b/mathlib4/Mathlib/RingTheory/Polynomial/Resultant/Basic.lean @@ -148,6 +148,7 @@ lemma resultant_map_map (φ : R →+* S) : theorem resultant_C_zero_left : resultant (C r) g 0 m = r ^ m := by simp set_option backward.defeqAttrib.useBackward true in +set_option dsimp.resynthInstances false in /-- `Res(f, g) = (-1)ᵐⁿ Res(g, f)` -/ lemma resultant_comm : resultant f g m n = (-1) ^ (m * n) * resultant g f n m := by rw [resultant, resultant, sylvester_comm, Matrix.det_reindex, Equiv.Perm.sign_eq_prod_prod_Ioi] diff --git a/mathlib4/Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean b/mathlib4/Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean index 838ad3fa8..c12de60dc 100644 --- a/mathlib4/Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean +++ b/mathlib4/Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean @@ -443,6 +443,7 @@ lemma UniversalFactorizationRing.factor₁_mul_factor₂ : set_option backward.isDefEq.respectTransparency false in attribute [-instance] leftModule in +set_option dsimp.resynthInstances false in /-- The universal factorization ring represents `S ↦ "factorizations of p into (monic deg m) * (monic deg k) in S"`. -/ def UniversalFactorizationRing.homEquiv : diff --git a/mathlib4/Mathlib/RingTheory/Smooth/NoetherianDescent.lean b/mathlib4/Mathlib/RingTheory/Smooth/NoetherianDescent.lean index f6ff5fc45..ffcf0e74f 100644 --- a/mathlib4/Mathlib/RingTheory/Smooth/NoetherianDescent.lean +++ b/mathlib4/Mathlib/RingTheory/Smooth/NoetherianDescent.lean @@ -203,6 +203,7 @@ end DescentAux variable (R A B) +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in /-- diff --git a/mathlib4/Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean b/mathlib4/Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean index 35f86bc67..4bb37edd1 100644 --- a/mathlib4/Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean +++ b/mathlib4/Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean @@ -53,6 +53,7 @@ noncomputable def cotangentComplexAux [Finite σ] (P : PreSubmersivePresentation Finsupp.linearEquivFunOnFinite S S σ ∘ₗ Finsupp.lcomapDomain _ P.map_inj ∘ₗ P.cotangentSpaceBasis.repr.toLinearMap ∘ₗ P.toExtension.cotangentComplex +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma cotangentComplexAux_apply [Finite σ] (P : PreSubmersivePresentation R S ι σ) diff --git a/mathlib4/Mathlib/RingTheory/Valuation/Basic.lean b/mathlib4/Mathlib/RingTheory/Valuation/Basic.lean index ed8b787f1..05682b171 100644 --- a/mathlib4/Mathlib/RingTheory/Valuation/Basic.lean +++ b/mathlib4/Mathlib/RingTheory/Valuation/Basic.lean @@ -462,6 +462,7 @@ lemma leAddSubgroup_monotone (v : Valuation R Γ₀) : Monotone v.leAddSubgroup open MonoidWithZeroHom MonoidWithZeroHom.ValueGroup₀ +set_option dsimp.resynthInstances false in /-- The restriction of a valuation so that it takes values in its `valueGroup₀`. -/ @[implicit_reducible] def restrict : Valuation R (ValueGroup₀ (.ofClass v)) where diff --git a/mathlib4/Mathlib/Topology/Algebra/Valued/ValuedField.lean b/mathlib4/Mathlib/Topology/Algebra/Valued/ValuedField.lean index 629b7e1b7..131c7c1f7 100644 --- a/mathlib4/Mathlib/Topology/Algebra/Valued/ValuedField.lean +++ b/mathlib4/Mathlib/Topology/Algebra/Valued/ValuedField.lean @@ -458,6 +458,7 @@ noncomputable def valueGroup₀_hom_extensionValuation : · simp [extensionValuation_apply_coe, hxy, ← hx, ← hy, hx0, hy0] set_option backward.isDefEq.respectTransparency.types false in +set_option dsimp.resynthInstances false in /-- The zero-preserving monoid homomorphism from the `ValueGroup₀` of the valuation on `K` to that of the extension to its completion. -/ noncomputable def valueGroup₀_equiv_extensionValuation : diff --git a/mathlib4/Mathlib/Topology/MetricSpace/GromovHausdorff.lean b/mathlib4/Mathlib/Topology/MetricSpace/GromovHausdorff.lean index 8b16fb6ac..7260d76f0 100644 --- a/mathlib4/Mathlib/Topology/MetricSpace/GromovHausdorff.lean +++ b/mathlib4/Mathlib/Topology/MetricSpace/GromovHausdorff.lean @@ -97,6 +97,7 @@ instance : Inhabited GHSpace := def GHSpace.Rep (p : GHSpace) : Type := (Quotient.out p : NonemptyCompacts ℓ_infty_ℝ) +set_option dsimp.resynthInstances false in theorem eq_toGHSpace_iff {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X] {p : NonemptyCompacts ℓ_infty_ℝ} : ⟦p⟧ = toGHSpace X ↔ ∃ Ψ : X → ℓ_infty_ℝ, Isometry Ψ ∧ range Ψ = p := by diff --git a/mathlib4/Mathlib/Topology/Sheaves/LocalPredicate.lean b/mathlib4/Mathlib/Topology/Sheaves/LocalPredicate.lean index 243541d64..fcc4e9eeb 100644 --- a/mathlib4/Mathlib/Topology/Sheaves/LocalPredicate.lean +++ b/mathlib4/Mathlib/Topology/Sheaves/LocalPredicate.lean @@ -320,6 +320,7 @@ theorem stalkToFiber_surjective (P : LocalPredicate T) (x : X) · exact (subsheafToTypes P).presheaf.germ _ x U.2 ⟨f, h⟩ · exact stalkToFiber_germ P U.1 x U.2 ⟨f, h⟩ +set_option dsimp.resynthInstances false in set_option backward.defeqAttrib.useBackward true in /-- The `stalkToFiber` map is injective at `x` if any two allowed sections which agree at `x` agree on some neighborhood of `x`. diff --git a/mathlib4/Mathlib/Topology/Sheaves/LocallySurjective.lean b/mathlib4/Mathlib/Topology/Sheaves/LocallySurjective.lean index 691f46d11..5f1955f67 100644 --- a/mathlib4/Mathlib/Topology/Sheaves/LocallySurjective.lean +++ b/mathlib4/Mathlib/Topology/Sheaves/LocallySurjective.lean @@ -74,6 +74,7 @@ section SurjectiveOnStalks variable [Limits.HasColimits C] [Limits.PreservesFilteredColimits (forget C)] +set_option dsimp.resynthInstances false in set_option backward.isDefEq.respectTransparency false in /-- An equivalent condition for a map of presheaves to be locally surjective is for all the induced maps on stalks to be surjective. -/ diff --git a/mathlib4/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean b/mathlib4/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean index 0d4026c00..dfec62a7f 100644 --- a/mathlib4/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean +++ b/mathlib4/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean @@ -458,6 +458,7 @@ protected theorem tendsto_iff_tendstoUniformly {F : ι → α →ᵤ β} {f : α simp only [mem_ofPred, UniformFun.gen, Function.comp_def] set_option backward.isDefEq.respectTransparency false in +set_option dsimp.resynthInstances false in /-- The natural bijection between `α → β × γ` and `(α → β) × (α → γ)`, upgraded to a uniform isomorphism between `α →ᵤ β × γ` and `(α →ᵤ β) × (α →ᵤ γ)`. -/ protected def uniformEquivProdArrow [UniformSpace γ] : (α →ᵤ β × γ) ≃ᵤ (α →ᵤ β) × (α →ᵤ γ) := diff --git a/mathlib4/lakefile.lean b/mathlib4/lakefile.lean index 77c474bc3..5b498e764 100644 --- a/mathlib4/lakefile.lean +++ b/mathlib4/lakefile.lean @@ -44,6 +44,7 @@ abbrev mathlibLeanOptions := #[ ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b` ⟨`autoImplicit, false⟩, ⟨`maxSynthPendingDepth, .ofNat 3⟩, + ⟨`backward.isDefEq.respectTransparency.instances, false⟩, ] ++ -- options that are used in `lake build` mathlibOnlyLinters.map fun s ↦ { s with name := `weak ++ s.name } diff --git a/mathlib4/persistent.md b/mathlib4/persistent.md new file mode 100644 index 000000000..956193d41 --- /dev/null +++ b/mathlib4/persistent.md @@ -0,0 +1,28 @@ +- Mathlib/Algebra/Category/AlgCat/TensorAlgebra.lean +- Mathlib/Algebra/Category/ModuleCat/Differentials/Basic.lean +- Mathlib/Algebra/Category/ModuleCat/Presheaf.lean +- Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean +- Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/UnionProd.lean +- Mathlib/AlgebraicTopology/SimplicialSet/Homotopy.lean +- Mathlib/Analysis/Calculus/IteratedDeriv/FaaDiBruno.lean +- Mathlib/Analysis/InnerProductSpace/PiL2.lean +- Mathlib/CategoryTheory/Bicategory/Yoneda.lean +- Mathlib/CategoryTheory/Grothendieck.lean +- Mathlib/CategoryTheory/Limits/Elements.lean +- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform.lean +- Mathlib/CategoryTheory/Monoidal/Cartesian/Ring.lean +- Mathlib/CategoryTheory/Monoidal/Mon.lean +- Mathlib/CategoryTheory/Preadditive/Mat.lean +- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean +- Mathlib/Data/DFinsupp/WellFounded.lean +- Mathlib/Data/Ordmap/Invariants.lean +- Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean +- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean +- Mathlib/Order/Birkhoff.lean +- Mathlib/Probability/ProbabilityMassFunction/Monad.lean +- Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean +- Mathlib/RingTheory/Extension/Generators.lean +- Mathlib/RingTheory/Morita/Matrix.lean +- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean +- Mathlib/Topology/Algebra/Valued/ValuedField.lean +- Mathlib/Topology/Sheaves/LocalPredicate.lean