Created
April 2, 2026 05:12
-
-
Save kim-em/ba1d233feae991cd75be80bb20c84ad3 to your computer and use it in GitHub Desktop.
Tier 2 @[simps] defeq warnings (126 cases, filtered)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| warning: Mathlib/Algebra/AddConstMap/Basic.lean:407:2: `@[simps]` generated lemma `AddConstMap.toEnd_apply : ⇑toEnd = DFunLike.coe` where the type of the LHS | |
| (G →+c[a✝¹, a✝¹] G) → Function.End G | |
| is not definitionally equal to the type of the RHS | |
| (G →+c[a✝¹, a✝¹] G) → G → G | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Algebra/Subalgebra/MulOpposite.lean:149:2: `@[simps]` generated lemma `Subalgebra.algEquivOpMop_apply : S.algEquivOpMop a✝ = | |
| MulOpposite.op (S.addEquivOp a✝)` where the type of the LHS | |
| (↥S.op)ᵐᵒᵖ | |
| is not definitionally equal to the type of the RHS | |
| (↥S.op)ᵐᵒᵖ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/DirectSum/AddChar.lean:28:2: `@[simps]` generated lemma `AddChar.directSum_apply : (directSum ψ) a✝ = | |
| (DirectSum.toAddMonoid fun i ↦ toAddMonoidHomEquiv (ψ i)) a✝` where the type of the LHS | |
| R | |
| is not definitionally equal to the type of the RHS | |
| Additive R | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/DirectSum/Basic.lean:321:2: `@[simps]` generated lemma `DirectSum.addEquivProdDirectSum_apply : addEquivProdDirectSum f = | |
| (f none, DFinsupp.comapDomain some ⋯ f)` where the type of the LHS | |
| α none × ⨁ (i : ι), α (some i) | |
| is not definitionally equal to the type of the RHS | |
| α none × Π₀ (i : ι), α (some i) | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/DirectSum/Basic.lean:321:2: `@[simps]` generated lemma `DirectSum.addEquivProdDirectSum_symm_apply_support' : (addEquivProdDirectSum.symm | |
| f).support' = | |
| Trunc.map (fun s ↦ ⟨none ::ₘ Multiset.map some ↑s, ⋯⟩) f.2.support'` where the type of the LHS | |
| Trunc { s // ∀ (i : Option ι), i ∈ s ∨ (addEquivProdDirectSum.symm f).toFun i = 0 } | |
| is not definitionally equal to the type of the RHS | |
| Trunc | |
| { s // | |
| ∀ (i : Option ι), | |
| i ∈ s ∨ | |
| (match i with | |
| | none => f.1 | |
| | some val => f.2 val) = | |
| 0 } | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Group/Action/Basic.lean:193:2: `@[simps]` generated lemma `MulDistribMulAction.toMonoidEnd_apply : (toMonoidEnd M A) r = | |
| toMonoidHom A r` where the type of the LHS | |
| Monoid.End A | |
| is not definitionally equal to the type of the RHS | |
| A →* A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Group/End.lean:88:2: `@[simps]` generated lemma `Equiv.Perm.equivUnitsEnd_symm_apply_apply : ⇑(equivUnitsEnd.symm u) = | |
| ↑u` where the type of the LHS | |
| α → α | |
| is not definitionally equal to the type of the RHS | |
| Function.End α | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Group/End.lean:88:2: `@[simps]` generated lemma `Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply : ⇑(Equiv.symm (equivUnitsEnd.symm u)) = | |
| ↑u⁻¹` where the type of the LHS | |
| α → α | |
| is not definitionally equal to the type of the RHS | |
| Function.End α | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Group/End.lean:97:2: `@[simps]` generated lemma `MonoidHom.toHomPerm_apply_apply : ⇑(f.toHomPerm a✝) = f a✝` where the type of the LHS | |
| α → α | |
| is not definitionally equal to the type of the RHS | |
| Function.End α | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Group/End.lean:97:2: `@[simps]` generated lemma `MonoidHom.toHomPerm_apply_symm_apply : ⇑(Equiv.symm (f.toHomPerm a✝)) = | |
| ↑(f.toHomUnits a✝)⁻¹` where the type of the LHS | |
| α → α | |
| is not definitionally equal to the type of the RHS | |
| Function.End α | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Group/Equiv/TypeTags.lean:194:2: `@[simps]` generated lemma `MulEquiv.Monoid.End_apply : End f = | |
| { toFun := fun a ↦ Additive.ofMul (f (Additive.toMul a)), map_zero' := ⋯, map_add' := ⋯ }` where the type of the LHS | |
| AddMonoid.End (Additive M) | |
| is not definitionally equal to the type of the RHS | |
| Additive M →+ Additive M | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Group/Equiv/TypeTags.lean:200:2: `@[simps]` generated lemma `MulEquiv.AddMonoid.End_apply : End f = | |
| { toFun := fun a ↦ Multiplicative.ofAdd (f (Multiplicative.toAdd a)), map_one' := ⋯, | |
| map_mul' := ⋯ }` where the type of the LHS | |
| _root_.Monoid.End (Multiplicative M) | |
| is not definitionally equal to the type of the RHS | |
| Multiplicative M →* Multiplicative M | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Group/Subgroup/Lattice.lean:65:2: `@[simps]` generated lemma `Subgroup.coe_toAddSubgroup_symm_apply : ↑((RelIso.symm toAddSubgroup) S) = | |
| ⇑Multiplicative.toAdd ⁻¹' ↑S` where the type of the LHS | |
| Set G | |
| is not definitionally equal to the type of the RHS | |
| Set (Multiplicative (Additive G)) | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Group/Subgroup/Lattice.lean:87:2: `@[simps]` generated lemma `AddSubgroup.coe_toSubgroup_symm_apply : ↑((RelIso.symm toSubgroup) S) = | |
| ⇑Additive.toMul ⁻¹' ↑S` where the type of the LHS | |
| Set A | |
| is not definitionally equal to the type of the RHS | |
| Set (Additive (Multiplicative A)) | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/GroupWithZero/Action/Defs.lean:391:2: `@[simps]` generated lemma `DistribMulAction.toAddMonoidEnd_apply : (toAddMonoidEnd M A) x = | |
| DistribSMul.toAddMonoidHom A x` where the type of the LHS | |
| AddMonoid.End A | |
| is not definitionally equal to the type of the RHS | |
| A →+ A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Lie/NonUnitalNonAssocAlgebra.lean:81:2: `@[simps]` generated lemma `LieHom.toNonUnitalAlgHom_apply : f.toNonUnitalAlgHom a = f a` where the type of the LHS | |
| CommutatorRing L₂ | |
| is not definitionally equal to the type of the RHS | |
| L₂ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Lie/NonUnitalNonAssocAlgebra.lean:81:2: `@[simps]` generated lemma `LieHom.toNonUnitalAlgHom_toFun : f.toNonUnitalAlgHom a = f a` where the type of the LHS | |
| CommutatorRing L₂ | |
| is not definitionally equal to the type of the RHS | |
| L₂ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Lie/Quotient.lean:221:2: `@[simps]` generated lemma `LieHom.quotKerEquivRange_invFun : f.quotKerEquivRange.invFun a✝ = | |
| (↑f).quotKerEquivRange.invFun a✝` where the type of the LHS | |
| L ⧸ f.ker | |
| is not definitionally equal to the type of the RHS | |
| L ⧸ (↑f).ker | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Lie/Quotient.lean:221:2: `@[simps]` generated lemma `LieHom.quotKerEquivRange_toFun : f.quotKerEquivRange a = | |
| (↑f).quotKerEquivRange a` where the type of the LHS | |
| ↥f.range | |
| is not definitionally equal to the type of the RHS | |
| ↥(↑f).range | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Lie/Weights/Linear.lean:205:2: `@[simps]` generated lemma `LieModule.shiftedGenWeightSpace.shift_apply : (shift R L M χ) a = | |
| a` where the type of the LHS | |
| ↥(shiftedGenWeightSpace R L M χ) | |
| is not definitionally equal to the type of the RHS | |
| ↥(genWeightSpace M χ) | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Module/CharacterModule.lean:80:2: `@[simps]` generated lemma `CharacterModule.dual_apply : (dual f) L = | |
| AddMonoidHom.comp L f.toAddMonoidHom` where the type of the LHS | |
| CharacterModule A | |
| is not definitionally equal to the type of the RHS | |
| A →+ AddCircle 1 | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Module/CharacterModule.lean:120:2: `@[simps]` generated lemma `CharacterModule.uncurry_apply : uncurry c = | |
| liftAddHom c.toAddMonoidHom ⋯` where the type of the LHS | |
| CharacterModule (A ⊗[R] B) | |
| is not definitionally equal to the type of the RHS | |
| A ⊗[R] B →+ AddCircle 1 | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Module/CharacterModule.lean:130:2: `@[simps]` generated lemma `CharacterModule.curry_apply_apply : (curry c) x✝ = | |
| AddMonoidHom.comp c ↑((mk R A B) x✝)` where the type of the LHS | |
| CharacterModule B | |
| is not definitionally equal to the type of the RHS | |
| B →+ AddCircle 1 | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Module/Equiv/Basic.lean:395:2: `@[simps]` generated lemma `addMonoidEndRingEquivInt_symm_apply : (addMonoidEndRingEquivInt A).symm a✝ = | |
| (addMonoidHomLequivInt ℤ).invFun a✝` where the type of the LHS | |
| AddMonoid.End A | |
| is not definitionally equal to the type of the RHS | |
| A →+ A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Module/Presentation/Basic.lean:510:2: `@[simps]` generated lemma `Module.Presentation.ofLinearEquiv_toSolution : (pres.ofLinearEquiv e).toSolution = | |
| pres.postcomp ↑e` where the type of the LHS | |
| (pres.ofLinearEquiv e).Solution N | |
| is not definitionally equal to the type of the RHS | |
| pres.Solution N | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Module/Presentation/Cokernel.lean:131:2: `@[simps]` generated lemma `Module.Presentation.cokernel_relation : (pres₂.cokernel data hg₁).relation x✝ = | |
| match x✝ with | |
| | Sum.inl r => pres₂.relation r | |
| | Sum.inr i => data.lift i` where the type of the LHS | |
| (pres₂.cokernel data hg₁).G →₀ A | |
| is not definitionally equal to the type of the RHS | |
| pres₂.G →₀ A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Module/Presentation/Cokernel.lean:140:2: `@[simps]` generated lemma `Module.Presentation.ofExact_relation : (pres₂.ofExact data hfg hg hg₁).relation x✝ = | |
| match x✝ with | |
| | Sum.inl r => pres₂.relation r | |
| | Sum.inr i => data.lift i` where the type of the LHS | |
| (pres₂.ofExact data hfg hg hg₁).G →₀ A | |
| is not definitionally equal to the type of the RHS | |
| pres₂.G →₀ A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Module/Presentation/DirectSum.lean:112:2: `@[simps]` generated lemma `Module.Presentation.directSum_relation : (directSum pres).relation x✝ = | |
| Finsupp.embDomain (Function.Embedding.sigmaMk x✝.fst) ((pres x✝.fst).relation x✝.snd)` where the type of the LHS | |
| (directSum pres).G →₀ A | |
| is not definitionally equal to the type of the RHS | |
| (i : ι) × (pres i).G →₀ A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Module/Presentation/DirectSum.lean:129:2: `@[simps]` generated lemma `Module.Presentation.finsupp_relation : (pres.finsupp ι).relation x✝ = | |
| Finsupp.embDomain (Function.Embedding.sigmaMk x✝.fst) (pres.relation x✝.snd)` where the type of the LHS | |
| (pres.finsupp ι).G →₀ A | |
| is not definitionally equal to the type of the RHS | |
| (i : ι) × pres.G →₀ A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Module/Presentation/Tautological.lean:84:2: `@[simps]` generated lemma `Module.Presentation.tautological_relation : (tautological A M).relation x✝ = | |
| match x✝ with | |
| | tautological.R.add m₁ m₂ => Finsupp.single m₁ 1 + Finsupp.single m₂ 1 - Finsupp.single (m₁ + m₂) 1 | |
| | tautological.R.smul a m => Finsupp.single m a - Finsupp.single (a • m) 1` where the type of the LHS | |
| (tautological A M).G →₀ A | |
| is not definitionally equal to the type of the RHS | |
| M →₀ A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Module/Submodule/Range.lean:143:2: `@[simps]` generated lemma `LinearMap.iterateRange_coe : f.iterateRange n = (f ^ n).range` where the type of the LHS | |
| (Submodule R M)ᵒᵈ | |
| is not definitionally equal to the type of the RHS | |
| Submodule R M | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Module/Submodule/RestrictScalars.lean:105:2: `@[simps]` generated lemma `Submodule.restrictScalarsEquiv_symm_apply : (restrictScalarsEquiv S R M p).symm a✝ = | |
| a✝` where the type of the LHS | |
| ↥(restrictScalars S p) | |
| is not definitionally equal to the type of the RHS | |
| ↥p | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/MonoidAlgebra/Defs.lean:637:45: `@[simps]` generated lemma `AddMonoidAlgebra.uniqueRingEquiv_symm_apply : (AddMonoidAlgebra.uniqueRingEquiv M).symm a✝ = | |
| equivFunOnFinite.symm (uniqueElim a✝)` where the type of the LHS | |
| AddMonoidAlgebra R M | |
| is not definitionally equal to the type of the RHS | |
| M →₀ R | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/MonoidAlgebra/Defs.lean:637:45: `@[simps]` generated lemma `MonoidAlgebra.uniqueRingEquiv_symm_apply : (uniqueRingEquiv M).symm a✝ = | |
| equivFunOnFinite.symm (uniqueElim a✝)` where the type of the LHS | |
| R[M] | |
| is not definitionally equal to the type of the RHS | |
| M →₀ R | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/MonoidAlgebra/Opposite.lean:29:45: `@[simps]` generated lemma `AddMonoidAlgebra.opRingEquiv_apply : AddMonoidAlgebra.opRingEquiv a✝ = | |
| equivMapDomain AddOpposite.opEquiv (mapRange op ⋯ (unop a✝))` where the type of the LHS | |
| AddMonoidAlgebra Rᵐᵒᵖ Mᵃᵒᵖ | |
| is not definitionally equal to the type of the RHS | |
| Mᵃᵒᵖ →₀ Rᵐᵒᵖ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/MonoidAlgebra/Opposite.lean:29:45: `@[simps]` generated lemma `AddMonoidAlgebra.opRingEquiv_symm_apply : AddMonoidAlgebra.opRingEquiv.symm a✝ = | |
| op (mapRange unop ⋯ (equivMapDomain AddOpposite.opEquiv.symm a✝))` where the type of the LHS | |
| (AddMonoidAlgebra R M)ᵐᵒᵖ | |
| is not definitionally equal to the type of the RHS | |
| (M →₀ R)ᵐᵒᵖ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/MonoidAlgebra/Opposite.lean:29:45: `@[simps]` generated lemma `MonoidAlgebra.opRingEquiv_apply : MonoidAlgebra.opRingEquiv a✝ = | |
| equivMapDomain opEquiv (mapRange op ⋯ (unop a✝))` where the type of the LHS | |
| Rᵐᵒᵖ[Mᵐᵒᵖ] | |
| is not definitionally equal to the type of the RHS | |
| Mᵐᵒᵖ →₀ Rᵐᵒᵖ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/MonoidAlgebra/Opposite.lean:29:45: `@[simps]` generated lemma `MonoidAlgebra.opRingEquiv_symm_apply : MonoidAlgebra.opRingEquiv.symm a✝ = | |
| op (mapRange unop ⋯ (equivMapDomain opEquiv.symm a✝))` where the type of the LHS | |
| R[M]ᵐᵒᵖ | |
| is not definitionally equal to the type of the RHS | |
| (M →₀ R)ᵐᵒᵖ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Quaternion.lean:703:2: `@[simps]` generated lemma `Quaternion.equivTuple_symm_apply : (equivTuple R).symm a = | |
| { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }` where the type of the LHS | |
| ℍ[R] | |
| is not definitionally equal to the type of the RHS | |
| ℍ[R,-1,-1] | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Ring/Subring/MulOpposite.lean:153:2: `@[simps]` generated lemma `Subring.ringEquivOpMop_apply : S.ringEquivOpMop a✝ = | |
| MulOpposite.op (S.addEquivOp a✝)` where the type of the LHS | |
| (↥S.op)ᵐᵒᵖ | |
| is not definitionally equal to the type of the RHS | |
| (↥S.op)ᵐᵒᵖ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/TrivSqZeroExt/Basic.lean:745:2: `@[simps]` generated lemma `TrivSqZeroExt.invertibleEquivInvertibleFst_symm_apply_invOf : ⅟x = | |
| (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst))` where the type of the LHS | |
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) | |
| is not definitionally equal to the type of the RHS | |
| R × M | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Algebra/Vertex/HVertexOperator.lean:110:2: `@[simps]` generated lemma `HVertexOperator.compHahnSeries_coeff : (A.compHahnSeries B u).coeff g' = | |
| A ((coeff B g') u)` where the type of the LHS | |
| HahnSeries Γ W | |
| is not definitionally equal to the type of the RHS | |
| HahnModule Γ R W | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Analysis/Normed/Affine/Isometry.lean:814:16: `@[simps]` generated lemma `AffineSubspace.equivMapOfInjective_toFun : (E.equivMapOfInjective φ hφ) p = | |
| ⟨φ ↑p, ⋯⟩` where the type of the LHS | |
| ↥(map φ E) | |
| is not definitionally equal to the type of the RHS | |
| { x // x ∈ ⇑φ '' ↑E } | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Analysis/Quaternion.lean:162:2: `@[simps]` generated lemma `Quaternion.linearIsometryEquivTuple_symm_apply : linearIsometryEquivTuple.symm a = | |
| { re := a.ofLp 0, imI := a.ofLp 1, imJ := a.ofLp 2, imK := a.ofLp 3 }` where the type of the LHS | |
| ℍ | |
| is not definitionally equal to the type of the RHS | |
| ℍ[ℝ,-1,-1] | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Combinatorics/Quiver/SingleObj.lean:69:2: `@[simps]` generated lemma `Quiver.SingleObj.toPrefunctor_apply_obj : (toPrefunctor f).obj a = | |
| id a` where the type of the LHS | |
| SingleObj β | |
| is not definitionally equal to the type of the RHS | |
| SingleObj α | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Combinatorics/Quiver/Symmetric.lean:156:2: `@[simps]` generated lemma `Quiver.Symmetrify.of_obj : of.obj a = id a` where the type of the LHS | |
| Symmetrify V | |
| is not definitionally equal to the type of the RHS | |
| V | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Combinatorics/Quiver/Symmetric.lean:204:2: `@[simps]` generated lemma `Prefunctor.symmetrify_obj : φ.symmetrify.obj a✝ = φ.obj a✝` where the type of the LHS | |
| Symmetrify V | |
| is not definitionally equal to the type of the RHS | |
| V | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Data/Bundle.lean:136:2: `@[simps]` generated lemma `Bundle.Pullback.lift_snd : (lift f a✝).snd = a✝.snd` where the type of the LHS | |
| E (lift f a✝).proj | |
| is not definitionally equal to the type of the RHS | |
| (f *ᵖ E) a✝.proj | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Data/Matrix/DualNumber.lean:26:2: `@[simps]` generated lemma `Matrix.dualNumberEquiv_apply : dualNumberEquiv A = | |
| (of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j))` where the type of the LHS | |
| DualNumber (Matrix n n R) | |
| is not definitionally equal to the type of the RHS | |
| Matrix n n R × Matrix n n R | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Data/Multiset/Fintype.lean:239:2: `@[simps]` generated lemma `Multiset.cast_symm_apply_snd : ((cast h).symm x).snd = | |
| Fin.cast ⋯ x.snd` where the type of the LHS | |
| Fin (count ((cast h).symm x).fst s) | |
| is not definitionally equal to the type of the RHS | |
| Fin (count x.fst s) | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Data/Real/ENatENNReal.lean:39:2: `@[simps]` generated lemma `ENat.toENNRealOrderEmbedding_apply : ⇑toENNRealOrderEmbedding = | |
| WithTop.map Nat.cast` where the type of the LHS | |
| ℕ∞ → ℝ≥0∞ | |
| is not definitionally equal to the type of the RHS | |
| WithTop ℕ → WithTop ℝ≥0 | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Data/Sym/Basic.lean:474:2: `@[simps]` generated lemma `Sym.oneEquiv_apply : oneEquiv a = ⟨{a}, ⋯⟩` where the type of the LHS | |
| Sym α 1 | |
| is not definitionally equal to the type of the RHS | |
| { s // s.card = 1 } | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean:400:2: `@[simps]` generated lemma `equivTangentBundleProd_symm_apply_snd : ((equivTangentBundleProd I M I' M').symm p).snd = | |
| (p.1.snd, p.2.snd)` where the type of the LHS | |
| TangentSpace (I.prod I') ((equivTangentBundleProd I M I' M').symm p).proj | |
| is not definitionally equal to the type of the RHS | |
| E × E' | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Geometry/Manifold/IsManifold/Basic.lean:500:2: `@[simps]` generated lemma `ModelWithCorners.prod_symm_apply : ↑(I.prod I').symm x = | |
| (↑I.symm x.1, ↑I'.symm x.2)` where the type of the LHS | |
| ModelProd H H' | |
| is not definitionally equal to the type of the RHS | |
| H × H' | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Geometry/Manifold/Sheaf/Smooth.lean:405:2: `@[simps]` generated lemma `ContMDiff.smoothSheafCommRingHom_hom_app_hom_apply : (CommRingCat.Hom.hom | |
| ((smoothSheafCommRingHom IP P f hf).hom.app U)) | |
| a✝ = | |
| (smoothSheafHom IP P f hf).hom.app U a✝` where the type of the LHS | |
| (smoothSheaf IM I M R).presheaf.obj ((Opens.map (TopCat.ofHom { toFun := f, continuous_toFun := ⋯ })).op.obj U) | |
| is not definitionally equal to the type of the RHS | |
| ((TopCat.Presheaf.pushforward (Type u) (TopCat.ofHom { toFun := f, continuous_toFun := ⋯ })).obj | |
| (smoothSheaf IM I M R).obj).obj | |
| U | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Geometry/RingedSpace/PresheafedSpace.lean:263:2: `@[simps]` generated lemma `AlgebraicGeometry.PresheafedSpace.restrict_presheaf : (X.restrict h).presheaf = | |
| h.functor.op ⋙ X.presheaf` where the type of the LHS | |
| Presheaf C ↑(X.restrict h) | |
| is not definitionally equal to the type of the RHS | |
| (Opens ↑U)ᵒᵖ ⥤ C | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/GroupTheory/FreeAbelianGroup.lean:197:2: `@[simps]` generated lemma `FreeAbelianGroup.liftAddEquiv_apply_apply : (liftAddEquiv a✝) a = | |
| Additive.ofMul ((Abelianization.lift (FreeGroup.lift a✝)) (Additive.toMul a))` where the type of the LHS | |
| G | |
| is not definitionally equal to the type of the RHS | |
| Additive (Multiplicative G) | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/GroupTheory/FreeAbelianGroup.lean:197:2: `@[simps]` generated lemma `FreeAbelianGroup.liftAddEquiv_symm_apply : liftAddEquiv.symm a✝¹ a✝ = | |
| (MonoidHom.toAdditive.symm a✝¹) (Abelianization.of (FreeGroup.of a✝))` where the type of the LHS | |
| G | |
| is not definitionally equal to the type of the RHS | |
| Multiplicative G | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean:206:2: `@[simps]` generated lemma `IsFreeGroupoid.SpanningTree.functorOfMonoidHom_obj : (functorOfMonoidHom T f).obj x✝ = | |
| ()` where the type of the LHS | |
| CategoryTheory.SingleObj X | |
| is not definitionally equal to the type of the RHS | |
| Unit | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/GroupTheory/Perm/Cycle/Type.lean:448:2: `@[simps]` generated lemma `Equiv.Perm.VectorsProdEqOne.vectorEquiv_symm_apply : (vectorEquiv G n).symm v = | |
| (↑v).tail` where the type of the LHS | |
| List.Vector G n | |
| is not definitionally equal to the type of the RHS | |
| List.Vector G (n + 1 - 1) | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/LinearAlgebra/ExteriorPower/Basic.lean:195:2: `@[simps]` generated lemma `exteriorPower.presentation_relation : (presentation R n M).relation x✝ = | |
| match x✝ with | |
| | presentation.Rels.add m i x y => | |
| Finsupp.single (update m i x) 1 + Finsupp.single (update m i y) 1 - Finsupp.single (update m i (x + y)) 1 | |
| | presentation.Rels.smul m i r x => Finsupp.single (update m i (r • x)) 1 - Finsupp.single (update m i x) r | |
| | presentation.Rels.alt m i j hm hij => Finsupp.single m 1` where the type of the LHS | |
| (presentation R n M).G →₀ R | |
| is not definitionally equal to the type of the RHS | |
| (Fin n → M) →₀ R | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Logic/Equiv/Basic.lean:426:2: `@[simps]` generated lemma `Equiv.sigmaAssocProd_apply_snd_snd : (sigmaAssocProd a✝).snd.snd = | |
| ((sigmaEquivProd α β).symm.sigmaCongrLeft' a✝).snd` where the type of the LHS | |
| γ ((sigmaEquivProd α β).symm.sigmaCongrLeft' a✝).fst.fst (sigmaAssocProd a✝).snd.fst | |
| is not definitionally equal to the type of the RHS | |
| γ ((sigmaEquivProd α β).symm.sigmaCongrLeft' a✝).fst.fst ((sigmaEquivProd α β).symm.sigmaCongrLeft' a✝).fst.snd | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Logic/Equiv/Basic.lean:426:2: `@[simps]` generated lemma `Equiv.sigmaAssocProd_symm_apply_snd : (sigmaAssocProd.symm a✝).snd = | |
| ((sigmaAssoc γ).symm a✝).snd` where the type of the LHS | |
| γ (sigmaAssocProd.symm a✝).fst.fst (sigmaAssocProd.symm a✝).fst.snd | |
| is not definitionally equal to the type of the RHS | |
| γ ((sigmaAssoc γ).symm a✝).fst.fst ((sigmaAssoc γ).symm a✝).fst.snd | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Logic/Equiv/Basic.lean:433:2: `@[simps]` generated lemma `Equiv.sigmaSubtype_symm_apply_coe_snd : (↑((sigmaSubtype a).symm b)).snd = | |
| b` where the type of the LHS | |
| β (↑((sigmaSubtype a).symm b)).fst | |
| is not definitionally equal to the type of the RHS | |
| β a | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Logic/Equiv/Fin/Basic.lean:45:2: `@[simps]` generated lemma `prodEquivPiFinTwo_apply : ⇑(prodEquivPiFinTwo α β) = fun p ↦ | |
| Fin.cons p.1 (Fin.cons p.2 finZeroElim)` where the type of the LHS | |
| α × β → (i : Fin 2) → ![α, β] i | |
| is not definitionally equal to the type of the RHS | |
| Fin.cons α (Fin.cons β finZeroElim) 0 × Fin.cons α (Fin.cons β finZeroElim) 1 → | |
| (i : Fin (1 + 1)) → Fin.cons α (Fin.cons β finZeroElim) i | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Logic/Equiv/Fin/Basic.lean:45:2: `@[simps]` generated lemma `prodEquivPiFinTwo_symm_apply : ⇑(prodEquivPiFinTwo α β).symm = fun f ↦ | |
| (f 0, f 1)` where the type of the LHS | |
| ((i : Fin 2) → ![α, β] i) → α × β | |
| is not definitionally equal to the type of the RHS | |
| ((i : Fin 2) → Fin.cons α (Fin.cons β finZeroElim) i) → | |
| Fin.cons α (Fin.cons β finZeroElim) 0 × Fin.cons α (Fin.cons β finZeroElim) 1 | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Logic/Function/FromTypes.lean:46:2: `@[simps]` generated lemma `Function.fromTypes_zero_equiv_apply : (fromTypes_zero_equiv p τ) a = | |
| a` where the type of the LHS | |
| τ | |
| is not definitionally equal to the type of the RHS | |
| FromTypes p τ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Logic/Function/FromTypes.lean:51:2: `@[simps]` generated lemma `Function.fromTypes_nil_equiv_apply : (fromTypes_nil_equiv τ) a = | |
| a` where the type of the LHS | |
| τ | |
| is not definitionally equal to the type of the RHS | |
| FromTypes ![] τ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Logic/Function/FromTypes.lean:57:2: `@[simps]` generated lemma `Function.fromTypes_succ_equiv_apply : (fromTypes_succ_equiv p τ) a = | |
| a` where the type of the LHS | |
| vecHead p → FromTypes (vecTail p) τ | |
| is not definitionally equal to the type of the RHS | |
| FromTypes p τ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Logic/Function/FromTypes.lean:63:2: `@[simps]` generated lemma `Function.fromTypes_cons_equiv_apply : (fromTypes_cons_equiv α p τ) a = | |
| a` where the type of the LHS | |
| α → FromTypes p τ | |
| is not definitionally equal to the type of the RHS | |
| FromTypes (vecCons α p) τ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/MeasureTheory/Integral/CompactlySupported.lean:48:2: `@[simps]` generated lemma `CompactlySupportedContinuousMap.integralLinearMap_apply : (integralLinearMap μ) f = | |
| ⟨∫ (x : X), ↑(f x) ∂μ, ⋯⟩` where the type of the LHS | |
| ℝ≥0 | |
| is not definitionally equal to the type of the RHS | |
| { r // 0 ≤ r } | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/ModelTheory/LanguageMap.lean:82:2: `@[simps]` generated lemma `FirstOrder.Language.LHom.sumInl_onFunction : LHom.sumInl.onFunction val = | |
| Sum.inl val` where the type of the LHS | |
| (L.sum L').Functions _n | |
| is not definitionally equal to the type of the RHS | |
| L.Functions _n ⊕ L'.Functions _n | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/ModelTheory/LanguageMap.lean:82:2: `@[simps]` generated lemma `FirstOrder.Language.LHom.sumInl_onRelation : LHom.sumInl.onRelation val = | |
| Sum.inl val` where the type of the LHS | |
| (L.sum L').Relations _n | |
| is not definitionally equal to the type of the RHS | |
| L.Relations _n ⊕ L'.Relations _n | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/ModelTheory/LanguageMap.lean:87:2: `@[simps]` generated lemma `FirstOrder.Language.LHom.sumInr_onFunction : LHom.sumInr.onFunction val = | |
| Sum.inr val` where the type of the LHS | |
| (L.sum L').Functions _n | |
| is not definitionally equal to the type of the RHS | |
| L.Functions _n ⊕ L'.Functions _n | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/ModelTheory/LanguageMap.lean:87:2: `@[simps]` generated lemma `FirstOrder.Language.LHom.sumInr_onRelation : LHom.sumInr.onRelation val = | |
| Sum.inr val` where the type of the LHS | |
| (L.sum L').Relations _n | |
| is not definitionally equal to the type of the RHS | |
| L.Relations _n ⊕ L'.Relations _n | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/ModelTheory/LanguageMap.lean:163:2: `@[simps]` generated lemma `FirstOrder.Language.LHom.sumMap_onFunction : (ϕ.sumMap ψ).onFunction a✝ = | |
| Sum.map (fun f ↦ ϕ.onFunction f) (fun f ↦ ψ.onFunction f) a✝` where the type of the LHS | |
| (L'.sum L₂).Functions _n | |
| is not definitionally equal to the type of the RHS | |
| L'.Functions _n ⊕ L₂.Functions _n | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/ModelTheory/LanguageMap.lean:163:2: `@[simps]` generated lemma `FirstOrder.Language.LHom.sumMap_onRelation : (ϕ.sumMap ψ).onRelation a✝ = | |
| Sum.map (fun f ↦ ϕ.onRelation f) (fun f ↦ ψ.onRelation f) a✝` where the type of the LHS | |
| (L'.sum L₂).Relations _n | |
| is not definitionally equal to the type of the RHS | |
| L'.Relations _n ⊕ L₂.Relations _n | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/ModelTheory/LanguageMap.lean:393:2: `@[simps]` generated lemma `FirstOrder.Language.lhomWithConstants_onFunction : (L.lhomWithConstants α).onFunction val = | |
| Sum.inl val` where the type of the LHS | |
| L[[α]].Functions _n | |
| is not definitionally equal to the type of the RHS | |
| L.Functions _n ⊕ | |
| match _n with | |
| | 0 => α | |
| | n.succ => PEmpty.{w' + 1} | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/ModelTheory/LanguageMap.lean:393:2: `@[simps]` generated lemma `FirstOrder.Language.lhomWithConstants_onRelation : (L.lhomWithConstants α).onRelation val = | |
| Sum.inl val` where the type of the LHS | |
| L[[α]].Relations _n | |
| is not definitionally equal to the type of the RHS | |
| L.Relations _n ⊕ Empty | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/ModelTheory/LanguageMap.lean:419:2: `@[simps]` generated lemma `FirstOrder.Language.LEquiv.addEmptyConstants_invLHom : (addEmptyConstants L α).invLHom = | |
| (LHom.id L).sumElim (LHom.ofIsEmpty (constantsOn α) L)` where the type of the LHS | |
| L[[α]] →ᴸ L | |
| is not definitionally equal to the type of the RHS | |
| L.sum (constantsOn α) →ᴸ L | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/CompleteSublattice.lean:207:2: `@[simps]` generated lemma `CompleteLatticeHom.toOrderIsoRangeOfInjective_apply : (f.toOrderIsoRangeOfInjective hf) a = | |
| ⟨f a, ⋯⟩` where the type of the LHS | |
| ↥f.range | |
| is not definitionally equal to the type of the RHS | |
| { x // x ∈ range ⇑(orderEmbeddingOfInjective f hf) } | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/Hom/Bounded.lean:476:19: `@[simps]` generated lemma `BotHom.dual_apply_apply : (BotHom.dual f) a = f a` where the type of the LHS | |
| βᵒᵈ | |
| is not definitionally equal to the type of the RHS | |
| β | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/Hom/Bounded.lean:476:19: `@[simps]` generated lemma `BotHom.dual_symm_apply_apply : (BotHom.dual.symm f) a = f a` where the type of the LHS | |
| β | |
| is not definitionally equal to the type of the RHS | |
| βᵒᵈ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/Hom/Bounded.lean:476:19: `@[simps]` generated lemma `TopHom.dual_apply_apply : (TopHom.dual f) a = f a` where the type of the LHS | |
| βᵒᵈ | |
| is not definitionally equal to the type of the RHS | |
| β | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/Hom/Bounded.lean:476:19: `@[simps]` generated lemma `TopHom.dual_symm_apply_apply : (TopHom.dual.symm f) a = f a` where the type of the LHS | |
| β | |
| is not definitionally equal to the type of the RHS | |
| βᵒᵈ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/Hom/BoundedLattice.lean:538:2: `@[simps]` generated lemma `BoundedLatticeHom.dual_apply_toFun : (BoundedLatticeHom.dual f) a = | |
| f a` where the type of the LHS | |
| βᵒᵈ | |
| is not definitionally equal to the type of the RHS | |
| β | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/Hom/BoundedLattice.lean:538:2: `@[simps]` generated lemma `BoundedLatticeHom.dual_symm_apply_toFun : (BoundedLatticeHom.dual.symm f) a = | |
| f a` where the type of the LHS | |
| β | |
| is not definitionally equal to the type of the RHS | |
| βᵒᵈ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/Hom/CompleteLattice.lean:587:2: `@[simps]` generated lemma `CompleteLatticeHom.dual_symm_apply_toFun : (CompleteLatticeHom.dual.symm f).toFun a✝ = | |
| toDual (f (ofDual a✝))` where the type of the LHS | |
| β | |
| is not definitionally equal to the type of the RHS | |
| βᵒᵈᵒᵈ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/Hom/Lattice.lean:525:19: `@[simps]` generated lemma `InfHom.dual_apply_toFun : (InfHom.dual f) a = f a` where the type of the LHS | |
| βᵒᵈ | |
| is not definitionally equal to the type of the RHS | |
| β | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/Hom/Lattice.lean:525:19: `@[simps]` generated lemma `InfHom.dual_symm_apply_toFun : (InfHom.dual.symm f) a = f a` where the type of the LHS | |
| β | |
| is not definitionally equal to the type of the RHS | |
| βᵒᵈ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/Hom/Lattice.lean:525:19: `@[simps]` generated lemma `SupHom.dual_apply_toFun : (SupHom.dual f) a = f a` where the type of the LHS | |
| βᵒᵈ | |
| is not definitionally equal to the type of the RHS | |
| β | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/Hom/Lattice.lean:525:19: `@[simps]` generated lemma `SupHom.dual_symm_apply_toFun : (SupHom.dual.symm f) a = f a` where the type of the LHS | |
| β | |
| is not definitionally equal to the type of the RHS | |
| βᵒᵈ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/Hom/Lattice.lean:557:2: `@[simps]` generated lemma `LatticeHom.dual_apply_toFun : (LatticeHom.dual f) a = f a` where the type of the LHS | |
| βᵒᵈ | |
| is not definitionally equal to the type of the RHS | |
| β | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/Hom/Lattice.lean:557:2: `@[simps]` generated lemma `LatticeHom.dual_symm_apply_toFun : (LatticeHom.dual.symm f) a = | |
| f a` where the type of the LHS | |
| β | |
| is not definitionally equal to the type of the RHS | |
| βᵒᵈ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/Sublattice.lean:357:2: `@[simps]` generated lemma `Sublattice.prodEquiv_symm_apply : (RelIso.symm (L.prodEquiv M)) x = | |
| ⟨(↑x.1, ↑x.2), ⋯⟩` where the type of the LHS | |
| ↥(L.prod M) | |
| is not definitionally equal to the type of the RHS | |
| { c // c.1 ∈ ↑L ∧ c.2 ∈ ↑M } | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Order/Sublattice.lean:357:2: `@[simps]` generated lemma `Sublattice.prodEquiv_toEquiv : (L.prodEquiv M).toEquiv = | |
| Equiv.Set.prod ↑L ↑M` where the type of the LHS | |
| ↥(L.prod M) ≃ ↥L × ↥M | |
| is not definitionally equal to the type of the RHS | |
| ↑(↑L ×ˢ ↑M) ≃ ↑↑L × ↑↑M | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RepresentationTheory/Basic.lean:510:2: `@[simps]` generated lemma `Representation.ofMulActionSelfAsModuleEquiv_apply : ofMulActionSelfAsModuleEquiv a✝ = | |
| (ofMulAction k G G).asModuleEquiv.toAddEquiv.toFun a✝` where the type of the LHS | |
| k[G] | |
| is not definitionally equal to the type of the RHS | |
| G →₀ k | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean:547:2: `@[simps]` generated lemma `groupCohomology.cocyclesOfIsCocycle₁_coe : ↑(cocyclesOfIsCocycle₁ hf) a✝ = | |
| f a✝` where the type of the LHS | |
| ↑(Rep.ofDistribMulAction k G A) | |
| is not definitionally equal to the type of the RHS | |
| A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean:560:2: `@[simps]` generated lemma `groupCohomology.coboundariesOfIsCoboundary₁_coe : ↑(coboundariesOfIsCoboundary₁ hf) a✝ = | |
| f a✝` where the type of the LHS | |
| ↑(Rep.ofDistribMulAction k G A) | |
| is not definitionally equal to the type of the RHS | |
| A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean:574:2: `@[simps]` generated lemma `groupCohomology.cocyclesOfIsCocycle₂_coe : ↑(cocyclesOfIsCocycle₂ hf) a✝ = | |
| f a✝` where the type of the LHS | |
| ↑(Rep.ofDistribMulAction k G A) | |
| is not definitionally equal to the type of the RHS | |
| A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean:586:2: `@[simps]` generated lemma `groupCohomology.coboundariesOfIsCoboundary₂_coe : ↑(coboundariesOfIsCoboundary₂ hf) a✝ = | |
| f a✝` where the type of the LHS | |
| ↑(Rep.ofDistribMulAction k G A) | |
| is not definitionally equal to the type of the RHS | |
| A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean:632:2: `@[simps]` generated lemma `groupHomology.cyclesOfIsCycle₁_coe : ↑(cyclesOfIsCycle₁ x hx) = x` where the type of the LHS | |
| G →₀ ↑(Rep.ofDistribMulAction k G A) | |
| is not definitionally equal to the type of the RHS | |
| G →₀ A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean:645:2: `@[simps]` generated lemma `groupHomology.boundariesOfIsBoundary₁_coe : ↑(boundariesOfIsBoundary₁ x hx) = | |
| x` where the type of the LHS | |
| G →₀ ↑(Rep.ofDistribMulAction k G A) | |
| is not definitionally equal to the type of the RHS | |
| G →₀ A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean:657:2: `@[simps]` generated lemma `groupHomology.cyclesOfIsCycle₂_coe : ↑(cyclesOfIsCycle₂ x hx) = x` where the type of the LHS | |
| G × G →₀ ↑(Rep.ofDistribMulAction k G A) | |
| is not definitionally equal to the type of the RHS | |
| G × G →₀ A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean:669:2: `@[simps]` generated lemma `groupHomology.boundariesOfIsBoundary₂_coe : ↑(boundariesOfIsBoundary₂ x hx) = | |
| x` where the type of the LHS | |
| G × G →₀ ↑(Rep.ofDistribMulAction k G A) | |
| is not definitionally equal to the type of the RHS | |
| G × G →₀ A | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RepresentationTheory/Rep/Basic.lean:388:2: `@[simps]` generated lemma `Rep.toAdditive_apply : toAdditive a = a` where the type of the LHS | |
| Additive G | |
| is not definitionally equal to the type of the RHS | |
| ↑(ofMulDistribMulAction M G) | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RingTheory/Extension/Basic.lean:262:2: `@[simps]` generated lemma `Algebra.Extension.toBaseChange_toRingHom : (toBaseChange T).toRingHom = | |
| TensorProduct.includeRight.toRingHom` where the type of the LHS | |
| P.Ring →+* P.baseChange.Ring | |
| is not definitionally equal to the type of the RHS | |
| P.Ring →+* T ⊗[R] P.Ring | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RingTheory/Extension/Cotangent/Basic.lean:417:2: `@[simps]` generated lemma `Algebra.Extension.H1Cotangent.equiv_apply : (equiv f₁ f₂) c = | |
| ⟨(Cotangent.map f₁) ↑c, ⋯⟩` where the type of the LHS | |
| P₂.H1Cotangent | |
| is not definitionally equal to the type of the RHS | |
| ↥(Submodule.restrictScalars S P₂.cotangentComplex.ker) | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RingTheory/Extension/Cotangent/Basic.lean:544:2: `@[simps]` generated lemma `Algebra.Generators.H1Cotangent.equiv_apply : (equiv P P') c = | |
| ⟨(Extension.Cotangent.map (P.defaultHom P').toExtensionHom) ↑c, ⋯⟩` where the type of the LHS | |
| P'.toExtension.H1Cotangent | |
| is not definitionally equal to the type of the RHS | |
| ↥(Submodule.restrictScalars S P'.toExtension.cotangentComplex.ker) | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RingTheory/Extension/Generators.lean:541:2: `@[simps]` generated lemma `Algebra.Generators.Hom.toExtensionHom_toRingHom : f.toExtensionHom.toRingHom = | |
| f.toAlgHom.toRingHom` where the type of the LHS | |
| P.toExtension.Ring →+* P'.toExtension.Ring | |
| is not definitionally equal to the type of the RHS | |
| P.Ring →+* P'.Ring | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RingTheory/HahnSeries/PowerSeries.lean:152:2: `@[simps]` generated lemma `HahnSeries.toMvPowerSeries_symm_apply_coeff : (toMvPowerSeries.symm f).coeff = | |
| f` where the type of the LHS | |
| (σ →₀ ℕ) → R | |
| is not definitionally equal to the type of the RHS | |
| MvPowerSeries σ R | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RingTheory/Ideal/Cotangent.lean:50:2: `@[simps]` generated lemma `Ideal.toCotangent_apply : I.toCotangent a✝ = | |
| Submodule.Quotient.mk a✝` where the type of the LHS | |
| I.Cotangent | |
| is not definitionally equal to the type of the RHS | |
| ↥I ⧸ I • ⊤ | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RingTheory/Ideal/Quotient/Operations.lean:528:2: `@[simps]` generated lemma `Ideal.quotientKerAlgEquivOfRightInverse_symm_apply : (quotientKerAlgEquivOfRightInverse | |
| hf).symm | |
| a✝ = | |
| (Quotient.mk (ker ↑f)) (g a✝)` where the type of the LHS | |
| A ⧸ ker f | |
| is not definitionally equal to the type of the RHS | |
| A ⧸ ker ↑f | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean:526:2: `@[simps]` generated lemma `rootsOfUnityEquivOfPrimitiveRoots_apply_coe_inv_val : ⋯ = ⋯` where the type of the LHS | |
| (↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ) a✝)).inv * ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ) a✝) = 1 | |
| is not definitionally equal to the type of the RHS | |
| ↑f (↑a✝).inv * ↑f ↑↑a✝ = 1 | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Topology/Algebra/Module/PointwiseConvergence.lean:134:2: `@[simps]` generated lemma `PointwiseConvergenceCLM.precomp_apply : (precomp G L) f = | |
| ContinuousLinearMap.comp f L` where the type of the LHS | |
| E →SLₚₜ[ρ] G | |
| is not definitionally equal to the type of the RHS | |
| E →SL[ρ] G | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Topology/Algebra/Module/PointwiseConvergence.lean:144:2: `@[simps]` generated lemma `PointwiseConvergenceCLM.postcomp_apply : (postcomp E L) f = | |
| L.comp f` where the type of the LHS | |
| E →SLₚₜ[ρ] G | |
| is not definitionally equal to the type of the RHS | |
| E →SL[ρ] G | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Topology/Algebra/Module/PointwiseConvergence.lean:152:2: `@[simps]` generated lemma `ContinuousLinearMap.toPointwiseConvergenceCLM_apply : (ContinuousLinearMap.toPointwiseConvergenceCLM | |
| 𝕜₂ σ E F) | |
| a = | |
| a` where the type of the LHS | |
| E →SLₚₜ[σ] F | |
| is not definitionally equal to the type of the RHS | |
| E →SL[σ] F | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Topology/Algebra/Module/PointwiseConvergence.lean:161:2: `@[simps]` generated lemma `PointwiseConvergenceCLM.equivWeakDual_apply : (equivWeakDual 𝕜 E) a = | |
| a` where the type of the LHS | |
| WeakDual 𝕜 E | |
| is not definitionally equal to the type of the RHS | |
| E →L[𝕜] 𝕜 | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Topology/Algebra/Module/PointwiseConvergence.lean:161:2: `@[simps]` generated lemma `PointwiseConvergenceCLM.equivWeakDual_symm_apply : (equivWeakDual 𝕜 E).symm a✝ = | |
| a✝` where the type of the LHS | |
| E →Lₚₜ[𝕜] 𝕜 | |
| is not definitionally equal to the type of the RHS | |
| E →L[𝕜] 𝕜 | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean:109:2: `@[simps]` generated lemma `ContinuousLinearMap.precompCompactConvergenceCLM_apply : (precompCompactConvergenceCLM G L) | |
| f = | |
| comp f L` where the type of the LHS | |
| E →SL_c[ρ] G | |
| is not definitionally equal to the type of the RHS | |
| E →SL[ρ] G | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean:123:2: `@[simps]` generated lemma `ContinuousLinearMap.postcompCompactConvergenceCLM_apply : (postcompCompactConvergenceCLM E | |
| L) | |
| f = | |
| L.comp f` where the type of the LHS | |
| E →SL_c[ρ] G | |
| is not definitionally equal to the type of the RHS | |
| E →SL[ρ] G | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean:440:2: `@[simps]` generated lemma `ContinuousLinearMap.precompUniformConvergenceCLM_apply : (precompUniformConvergenceCLM G 𝔖 𝔗 | |
| L hL) | |
| f = | |
| comp f L` where the type of the LHS | |
| UniformConvergenceCLM ρ G 𝔖 | |
| is not definitionally equal to the type of the RHS | |
| E →SL[ρ] G | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean:462:2: `@[simps]` generated lemma `ContinuousLinearMap.postcompUniformConvergenceCLM_apply : (postcompUniformConvergenceCLM 𝔖 | |
| L) | |
| f = | |
| L.comp f` where the type of the LHS | |
| UniformConvergenceCLM ρ G 𝔖 | |
| is not definitionally equal to the type of the RHS | |
| E →SL[ρ] G | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Topology/FiberBundle/Constructions.lean:193:2: `@[simps]` generated lemma `Bundle.Trivialization.prod_symm_apply_snd : (↑(e₁.prod e₂).symm p).snd = | |
| (e₁.symm p.1 p.2.1, e₂.symm p.1 p.2.2)` where the type of the LHS | |
| E₁ (↑(e₁.prod e₂).symm p).proj × E₂ (↑(e₁.prod e₂).symm p).proj | |
| is not definitionally equal to the type of the RHS | |
| E₁ p.1 × E₂ p.1 | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Topology/FiberBundle/Constructions.lean:305:2: `@[simps]` generated lemma `Bundle.Trivialization.pullback_symm_apply_snd : (↑(e.pullback f).symm y).snd = | |
| e.symm (f y.1) y.2` where the type of the LHS | |
| (⇑f *ᵖ E) (↑(e.pullback f).symm y).proj | |
| is not definitionally equal to the type of the RHS | |
| E (f y.1) | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
| warning: Mathlib/Topology/Sheaves/LocalPredicate.lean:281:2: `@[simps]` generated lemma `TopCat.subsheafToTypes_obj : (subsheafToTypes P).obj = | |
| subpresheafToTypes P.toPrelocalPredicate` where the type of the LHS | |
| (Opens ↑X)ᵒᵖ ⥤ Type (max u_2 u_1) | |
| is not definitionally equal to the type of the RHS | |
| Presheaf (Type (max u_1 u_2)) X | |
| Use `set_option simps.defeqWarn false in` to suppress this warning. | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment