From 1cef558b5941040b04b6349683c9ca6685802552 Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Wed, 13 Dec 2023 12:09:00 -0500 Subject: [PATCH 1/9] changes --- Mathlib/Algebra/Algebra/Basic.lean | 8 +++--- Mathlib/Algebra/Group/Hom/Defs.lean | 2 +- Mathlib/Algebra/Ring/Hom/Defs.lean | 8 ++++-- Mathlib/Analysis/NormedSpace/Basic.lean | 5 ++++ Mathlib/LinearAlgebra/Basis.lean | 1 + scratch.lean | 38 +++++++++++++++++++++++++ 6 files changed, 54 insertions(+), 8 deletions(-) create mode 100644 scratch.lean diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean index a453eaa8c28a2..5f7ecdcff0172 100644 --- a/Mathlib/Algebra/Algebra/Basic.lean +++ b/Mathlib/Algebra/Algebra/Basic.lean @@ -247,7 +247,7 @@ end FieldDivisionRing end algebraMap /-- Creating an algebra from a morphism to the center of a semiring. -/ -def RingHom.toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S) +@[reducible] def RingHom.toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S) (h : ∀ c x, i c * x = x * i c) : Algebra R S where smul c x := i c * x commutes' := h @@ -256,7 +256,7 @@ def RingHom.toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R →+* S) #align ring_hom.to_algebra' RingHom.toAlgebra' /-- Creating an algebra from a morphism to a commutative semiring. -/ -def RingHom.toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) : Algebra R S := +@[reducible] def RingHom.toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) : Algebra R S := i.toAlgebra' fun _ => mul_comm _ #align ring_hom.to_algebra RingHom.toAlgebra @@ -431,8 +431,8 @@ theorem coe_linearMap : ⇑(Algebra.linearMap R A) = algebraMap R A := rfl #align algebra.coe_linear_map Algebra.coe_linearMap -instance id : Algebra R R := - (RingHom.id R).toAlgebra +@[reducible] instance id : Algebra R R := + { (RingHom.id R).toAlgebra with } #align algebra.id Algebra.id variable {R A} diff --git a/Mathlib/Algebra/Group/Hom/Defs.lean b/Mathlib/Algebra/Group/Hom/Defs.lean index f8a707bc23a78..61a6d6b2af838 100644 --- a/Mathlib/Algebra/Group/Hom/Defs.lean +++ b/Mathlib/Algebra/Group/Hom/Defs.lean @@ -997,7 +997,7 @@ def MulHom.id (M : Type*) [Mul M] : M →ₙ* M where #align mul_hom.id_apply MulHom.id_apply /-- The identity map from a monoid to itself. -/ -@[to_additive (attr := simps)] +@[to_additive (attr := simps, reducible)] def MonoidHom.id (M : Type*) [MulOneClass M] : M →* M where toFun x := x map_one' := rfl diff --git a/Mathlib/Algebra/Ring/Hom/Defs.lean b/Mathlib/Algebra/Ring/Hom/Defs.lean index f1de7e94319a4..93be1fec35d5a 100644 --- a/Mathlib/Algebra/Ring/Hom/Defs.lean +++ b/Mathlib/Algebra/Ring/Hom/Defs.lean @@ -197,7 +197,7 @@ end variable [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] /-- The identity non-unital ring homomorphism from a non-unital semiring to itself. -/ -protected def id (α : Type*) [NonUnitalNonAssocSemiring α] : α →ₙ+* α := by +@[reducible] protected def id (α : Type*) [NonUnitalNonAssocSemiring α] : α →ₙ+* α := by refine' { toFun := id.. } <;> intros <;> rfl #align non_unital_ring_hom.id NonUnitalRingHom.id @@ -629,9 +629,11 @@ def mk' [NonAssocSemiring α] [NonAssocRing β] (f : α →* β) variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} /-- The identity ring homomorphism from a semiring to itself. -/ -def id (α : Type*) [NonAssocSemiring α] : α →+* α := by - refine' { toFun := _root_.id.. } <;> intros <;> rfl +@[reducible] def id (α : Type*) [NonAssocSemiring α] : α →+* α := + { AddMonoidHom.id α, MonoidHom.id α with } + -- refine' { toFun := _root_.id.. } <;> intros <;> rfl #align ring_hom.id RingHom.id +#print id instance : Inhabited (α →+* α) := ⟨id α⟩ diff --git a/Mathlib/Analysis/NormedSpace/Basic.lean b/Mathlib/Analysis/NormedSpace/Basic.lean index ecc9815a46f51..933a073f868d7 100644 --- a/Mathlib/Analysis/NormedSpace/Basic.lean +++ b/Mathlib/Analysis/NormedSpace/Basic.lean @@ -478,6 +478,11 @@ instance NormedAlgebra.id : NormedAlgebra 𝕜 𝕜 := { NormedField.toNormedSpace, Algebra.id 𝕜 with } #align normed_algebra.id NormedAlgebra.id +set_option pp.all true in +#print NormedAlgebra.id +set_option pp.all true in +#print Algebra.id + -- Porting note: cannot synth scalar tower ℚ ℝ k /-- Any normed characteristic-zero division ring that is a normed algebra over the reals is also a normed algebra over the rationals. diff --git a/Mathlib/LinearAlgebra/Basis.lean b/Mathlib/LinearAlgebra/Basis.lean index 8cbbd25f04307..5c19ae9e17027 100644 --- a/Mathlib/LinearAlgebra/Basis.lean +++ b/Mathlib/LinearAlgebra/Basis.lean @@ -1394,6 +1394,7 @@ def Submodule.inductionOnRankAux (b : Basis ι R M) (P : Submodule R M → Sort* end Induction +set_option maxHeartbeats 1000000 in /-- An element of a non-unital-non-associative algebra is in the center exactly when it commutes with the basis elements. -/ lemma Basis.mem_center_iff {A} diff --git a/scratch.lean b/scratch.lean new file mode 100644 index 0000000000000..197994d38e14c --- /dev/null +++ b/scratch.lean @@ -0,0 +1,38 @@ +import Mathlib.Data.Pi.Algebra +-- import Mathlib.Analysis.NormedSpace.Basic +import Mathlib.Algebra.Algebra.Basic +import Mathlib.Data.Real.Basic + +-- Example 1: succeeds +example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) : + (r • f) a = r • (f a) := by + simp only [Pi.smul_apply] -- succeeds + +-- Example 2: fails! +example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) : + (r • f) a = r • (f a) := by + let bar : SMul R R := SMulZeroClass.toSMul + simp only [Pi.smul_apply] -- Fails! + +set_option trace.Meta.synthInstance true in +def foo : Algebra.toSMul = SMulZeroClass.toSMul (M := ℝ) (A := ℝ) := by with_reducible_and_instances rfl +def bar : Algebra.toSMul = SMulZeroClass.toSMul (M := ℝ) (A := ℝ) := rfl + +set_option pp.all true in +#print foo + +set_option pp.all true in +#print bar + +/- +@rfl.{1} (SMul.{0, 0} Real Real) + (@Algebra.toSMul.{0, 0} Real Real Real.instCommSemiringReal Real.semiring + (@NormedAlgebra.toAlgebra.{0, 0} Real Real Real.normedField + (@SeminormedCommRing.toSeminormedRing.{0} Real + (@NormedCommRing.toSeminormedCommRing.{0} Real Real.normedCommRing)) + (@NormedAlgebra.id.{0} Real Real.normedField))) + +@rfl.{1} (SMul.{0, 0} Real Real) + (@Algebra.toSMul.{0, 0} Real Real Real.instCommSemiringReal Real.semiring + (@Algebra.id.{0} Real Real.instCommSemiringReal)) +-/ From c202f8364c46cc7f1a15a4514b938dbc4ad21edb Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Wed, 13 Dec 2023 12:09:36 -0500 Subject: [PATCH 2/9] rm --- scratch.lean | 38 -------------------------------------- 1 file changed, 38 deletions(-) delete mode 100644 scratch.lean diff --git a/scratch.lean b/scratch.lean deleted file mode 100644 index 197994d38e14c..0000000000000 --- a/scratch.lean +++ /dev/null @@ -1,38 +0,0 @@ -import Mathlib.Data.Pi.Algebra --- import Mathlib.Analysis.NormedSpace.Basic -import Mathlib.Algebra.Algebra.Basic -import Mathlib.Data.Real.Basic - --- Example 1: succeeds -example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) : - (r • f) a = r • (f a) := by - simp only [Pi.smul_apply] -- succeeds - --- Example 2: fails! -example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) : - (r • f) a = r • (f a) := by - let bar : SMul R R := SMulZeroClass.toSMul - simp only [Pi.smul_apply] -- Fails! - -set_option trace.Meta.synthInstance true in -def foo : Algebra.toSMul = SMulZeroClass.toSMul (M := ℝ) (A := ℝ) := by with_reducible_and_instances rfl -def bar : Algebra.toSMul = SMulZeroClass.toSMul (M := ℝ) (A := ℝ) := rfl - -set_option pp.all true in -#print foo - -set_option pp.all true in -#print bar - -/- -@rfl.{1} (SMul.{0, 0} Real Real) - (@Algebra.toSMul.{0, 0} Real Real Real.instCommSemiringReal Real.semiring - (@NormedAlgebra.toAlgebra.{0, 0} Real Real Real.normedField - (@SeminormedCommRing.toSeminormedRing.{0} Real - (@NormedCommRing.toSeminormedCommRing.{0} Real Real.normedCommRing)) - (@NormedAlgebra.id.{0} Real Real.normedField))) - -@rfl.{1} (SMul.{0, 0} Real Real) - (@Algebra.toSMul.{0, 0} Real Real Real.instCommSemiringReal Real.semiring - (@Algebra.id.{0} Real Real.instCommSemiringReal)) --/ From 1eba8514465e3b5d3b36ead5c260c566c5c84061 Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Wed, 13 Dec 2023 12:30:46 -0500 Subject: [PATCH 3/9] clean up --- Mathlib/Algebra/Algebra/Basic.lean | 5 +++-- Mathlib/Algebra/Ring/Hom/Defs.lean | 4 +--- Mathlib/Analysis/NormedSpace/Basic.lean | 5 ----- 3 files changed, 4 insertions(+), 10 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean index 5f7ecdcff0172..513aa1fd4bf59 100644 --- a/Mathlib/Algebra/Algebra/Basic.lean +++ b/Mathlib/Algebra/Algebra/Basic.lean @@ -256,7 +256,8 @@ end algebraMap #align ring_hom.to_algebra' RingHom.toAlgebra' /-- Creating an algebra from a morphism to a commutative semiring. -/ -@[reducible] def RingHom.toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) : Algebra R S := +@[reducible] def RingHom.toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) : + Algebra R S := i.toAlgebra' fun _ => mul_comm _ #align ring_hom.to_algebra RingHom.toAlgebra @@ -432,7 +433,7 @@ theorem coe_linearMap : ⇑(Algebra.linearMap R A) = algebraMap R A := #align algebra.coe_linear_map Algebra.coe_linearMap @[reducible] instance id : Algebra R R := - { (RingHom.id R).toAlgebra with } + (RingHom.id R).toAlgebra #align algebra.id Algebra.id variable {R A} diff --git a/Mathlib/Algebra/Ring/Hom/Defs.lean b/Mathlib/Algebra/Ring/Hom/Defs.lean index 93be1fec35d5a..2c06293b3a45a 100644 --- a/Mathlib/Algebra/Ring/Hom/Defs.lean +++ b/Mathlib/Algebra/Ring/Hom/Defs.lean @@ -197,7 +197,7 @@ end variable [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] /-- The identity non-unital ring homomorphism from a non-unital semiring to itself. -/ -@[reducible] protected def id (α : Type*) [NonUnitalNonAssocSemiring α] : α →ₙ+* α := by +protected def id (α : Type*) [NonUnitalNonAssocSemiring α] : α →ₙ+* α := by refine' { toFun := id.. } <;> intros <;> rfl #align non_unital_ring_hom.id NonUnitalRingHom.id @@ -631,9 +631,7 @@ variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} /-- The identity ring homomorphism from a semiring to itself. -/ @[reducible] def id (α : Type*) [NonAssocSemiring α] : α →+* α := { AddMonoidHom.id α, MonoidHom.id α with } - -- refine' { toFun := _root_.id.. } <;> intros <;> rfl #align ring_hom.id RingHom.id -#print id instance : Inhabited (α →+* α) := ⟨id α⟩ diff --git a/Mathlib/Analysis/NormedSpace/Basic.lean b/Mathlib/Analysis/NormedSpace/Basic.lean index 933a073f868d7..ecc9815a46f51 100644 --- a/Mathlib/Analysis/NormedSpace/Basic.lean +++ b/Mathlib/Analysis/NormedSpace/Basic.lean @@ -478,11 +478,6 @@ instance NormedAlgebra.id : NormedAlgebra 𝕜 𝕜 := { NormedField.toNormedSpace, Algebra.id 𝕜 with } #align normed_algebra.id NormedAlgebra.id -set_option pp.all true in -#print NormedAlgebra.id -set_option pp.all true in -#print Algebra.id - -- Porting note: cannot synth scalar tower ℚ ℝ k /-- Any normed characteristic-zero division ring that is a normed algebra over the reals is also a normed algebra over the rationals. From 0be03f5d4c34a973a99cdb7aa9b83f43eb7a66de Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Wed, 13 Dec 2023 12:54:44 -0500 Subject: [PATCH 4/9] timeout --- Mathlib/LinearAlgebra/Prod.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/LinearAlgebra/Prod.lean b/Mathlib/LinearAlgebra/Prod.lean index 5749201ff8828..a9d081aebcfe0 100644 --- a/Mathlib/LinearAlgebra/Prod.lean +++ b/Mathlib/LinearAlgebra/Prod.lean @@ -273,6 +273,7 @@ theorem coprod_map_prod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (S : Su exact Set.image_prod fun m m₂ => f m + g m₂ #align linear_map.coprod_map_prod LinearMap.coprod_map_prod +set_option maxHeartbeats 400000 in /-- Taking the product of two maps with the same codomain is equivalent to taking the product of their domains. From 2e75648185f098301a2797d604566eaeca0bafe6 Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Wed, 13 Dec 2023 12:55:55 -0500 Subject: [PATCH 5/9] timeout --- Mathlib/LinearAlgebra/Basis.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Basis.lean b/Mathlib/LinearAlgebra/Basis.lean index 5c19ae9e17027..f92d8db4069ca 100644 --- a/Mathlib/LinearAlgebra/Basis.lean +++ b/Mathlib/LinearAlgebra/Basis.lean @@ -1394,7 +1394,7 @@ def Submodule.inductionOnRankAux (b : Basis ι R M) (P : Submodule R M → Sort* end Induction -set_option maxHeartbeats 1000000 in +set_option maxHeartbeats 3200000 in /-- An element of a non-unital-non-associative algebra is in the center exactly when it commutes with the basis elements. -/ lemma Basis.mem_center_iff {A} From 948be641c497d4e68c536d75dee9526aea12d4bc Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Wed, 13 Dec 2023 13:44:15 -0500 Subject: [PATCH 6/9] timeouts --- Mathlib/Algebra/Lie/BaseChange.lean | 1 + Mathlib/Algebra/Lie/Submodule.lean | 2 +- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean | 1 + Mathlib/Analysis/Calculus/LagrangeMultipliers.lean | 1 + Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean | 1 - Mathlib/Analysis/SpecialFunctions/PolarCoord.lean | 1 + Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean | 1 + Mathlib/Geometry/Manifold/Instances/Sphere.lean | 1 + Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean | 2 +- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean | 2 ++ Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean | 2 ++ Mathlib/RepresentationTheory/Character.lean | 1 + Mathlib/RepresentationTheory/GroupCohomology/Basic.lean | 1 + Mathlib/RingTheory/Kaehler.lean | 2 +- Mathlib/RingTheory/PowerSeries/Basic.lean | 1 + 15 files changed, 16 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Lie/BaseChange.lean b/Mathlib/Algebra/Lie/BaseChange.lean index f7d73e38f5afb..968e3c5dfbb67 100644 --- a/Mathlib/Algebra/Lie/BaseChange.lean +++ b/Mathlib/Algebra/Lie/BaseChange.lean @@ -60,6 +60,7 @@ private theorem bracket_def (x : A ⊗[R] L) (m : A ⊗[R] M) : ⁅x, m⁆ = bra theorem bracket_tmul (s t : A) (x : L) (y : M) : ⁅s ⊗ₜ[R] x, t ⊗ₜ[R] y⁆ = (s * t) ⊗ₜ ⁅x, y⁆ := rfl #align lie_algebra.extend_scalars.bracket_tmul LieAlgebra.ExtendScalars.bracket_tmul +set_option maxHeartbeats 12800000 in private theorem bracket_lie_self (x : A ⊗[R] L) : ⁅x, x⁆ = 0 := by simp only [bracket_def] refine' x.induction_on _ _ _ diff --git a/Mathlib/Algebra/Lie/Submodule.lean b/Mathlib/Algebra/Lie/Submodule.lean index 5034a2247a6e9..c4582ca7af9f2 100644 --- a/Mathlib/Algebra/Lie/Submodule.lean +++ b/Mathlib/Algebra/Lie/Submodule.lean @@ -823,7 +823,7 @@ def map : LieSubmodule R L M' := lie_mem := fun {x m'} h ↦ by rcases h with ⟨m, hm, hfm⟩; use ⁅x, m⁆; constructor · apply N.lie_mem hm - · norm_cast at hfm; simp [hfm] } + · norm_cast at hfm; simp only [LieModuleHom.coe_toLinearMap, LieModuleHom.map_lie]; erw [hfm]} #align lie_submodule.map LieSubmodule.map @[simp] theorem coe_map : (N.map f : Set M') = f '' N := rfl diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean index 7f43e8d3c3f0a..61ceca68c4481 100644 --- a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean +++ b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean @@ -404,6 +404,7 @@ theorem mem_carrier_iff' (q : Spec.T A⁰_ f) (a : A) : dsimp only [Subtype.coe_mk]; rw [← hx]; rfl) #align algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.mem_carrier_iff' AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff' +set_option maxHeartbeats 400000 in theorem carrier.add_mem (q : Spec.T A⁰_ f) {a b : A} (ha : a ∈ carrier f_deg q) (hb : b ∈ carrier f_deg q) : a + b ∈ carrier f_deg q := by refine' fun i => (q.2.mem_or_mem _).elim id id diff --git a/Mathlib/Analysis/Calculus/LagrangeMultipliers.lean b/Mathlib/Analysis/Calculus/LagrangeMultipliers.lean index abe4e444c4d33..535b49a50ab75 100644 --- a/Mathlib/Analysis/Calculus/LagrangeMultipliers.lean +++ b/Mathlib/Analysis/Calculus/LagrangeMultipliers.lean @@ -121,6 +121,7 @@ theorem IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt {ι : Type*} [Fint · ext x; simpa [mul_comm] using hsum x #align is_local_extr_on.exists_multipliers_of_has_strict_fderiv_at IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt +set_option maxHeartbeats 400000 in /-- Lagrange multipliers theorem. Let `f : ι → E → ℝ` be a finite family of functions. Suppose that `φ : E → ℝ` has a local extremum on the set `{x | ∀ i, f i x = f i x₀}` at `x₀`. Suppose that all functions `f i` as well as `φ` are strictly differentiable at `x₀`. diff --git a/Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean b/Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean index 0ff228a39b066..4a3890abc8e9f 100644 --- a/Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean +++ b/Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean @@ -106,7 +106,6 @@ theorem WeakDual.CharacterSpace.mem_spectrum_iff_exists {a : A} {z : ℂ} : simp only [map_sub, sub_eq_zero, AlgHomClass.commutes, Algebra.id.map_eq_id, RingHom.id_apply] at hf refine ⟨f, ?_⟩ - rw [AlgHomClass.commutes, Algebra.id.map_eq_id, RingHom.id_apply] at hf exact hf.symm · rintro ⟨f, rfl⟩ exact AlgHom.apply_mem_spectrum f a diff --git a/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean b/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean index 80db011c91c89..4e91533655e82 100644 --- a/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean +++ b/Mathlib/Analysis/SpecialFunctions/PolarCoord.lean @@ -91,6 +91,7 @@ def polarCoord : PartialHomeomorph (ℝ × ℝ) (ℝ × ℝ) where · exact Complex.equivRealProdClm.symm.continuous.continuousOn #align polar_coord polarCoord +set_option maxHeartbeats 800000 in theorem hasFDerivAt_polarCoord_symm (p : ℝ × ℝ) : HasFDerivAt polarCoord.symm (LinearMap.toContinuousLinearMap (Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ) diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean index 41bded1ec1b11..c2504514b6fc3 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean @@ -28,6 +28,7 @@ open Filter namespace Complex +set_option maxHeartbeats 1600000 in theorem hasStrictFDerivAt_cpow {p : ℂ × ℂ} (hp : 0 < p.1.re ∨ p.1.im ≠ 0) : HasStrictFDerivAt (fun x : ℂ × ℂ => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ + diff --git a/Mathlib/Geometry/Manifold/Instances/Sphere.lean b/Mathlib/Geometry/Manifold/Instances/Sphere.lean index c838ca17e7a53..9d6fcd7743a54 100644 --- a/Mathlib/Geometry/Manifold/Instances/Sphere.lean +++ b/Mathlib/Geometry/Manifold/Instances/Sphere.lean @@ -142,6 +142,7 @@ theorem stereoInvFunAux_mem (hv : ‖v‖ = 1) {w : E} (hw : w ∈ (ℝ ∙ v) ring #align stereo_inv_fun_aux_mem stereoInvFunAux_mem +set_option synthInstance.maxHeartbeats 50000 in theorem hasFDerivAt_stereoInvFunAux (v : E) : HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0 := by have h₀ : HasFDerivAt (fun w : E => ‖w‖ ^ 2) (0 : E →L[ℝ] ℝ) 0 := by diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean index 694a974931491..d671c185c90a4 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean @@ -295,7 +295,7 @@ def toQuaternion : CliffordAlgebra (Q c₁ c₂) →ₐ[R] ℍ[R,c₁,c₂] := CliffordAlgebra.lift (Q c₁ c₂) ⟨{ toFun := fun v => (⟨0, v.1, v.2, 0⟩ : ℍ[R,c₁,c₂]) map_add' := fun v₁ v₂ => by simp - map_smul' := fun r v => by dsimp; rw [mul_zero]; rfl }, fun v => by + map_smul' := fun r v => by dsimp; rw [mul_zero] }, fun v => by dsimp ext all_goals dsimp; ring⟩ diff --git a/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean b/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean index 0459aff303ab3..2a0b07b520098 100644 --- a/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean +++ b/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean @@ -216,6 +216,7 @@ theorem BilinForm.toMatrix'_apply (B : BilinForm R₂ (n → R₂)) (i j : n) : rfl #align bilin_form.to_matrix'_apply BilinForm.toMatrix'_apply +set_option maxHeartbeats 1600000 in -- Porting note: dot notation for bundled maps doesn't work in the rest of this section @[simp] theorem BilinForm.toMatrix'_comp (B : BilinForm R₂ (n → R₂)) (l r : (o → R₂) →ₗ[R₂] n → R₂) : @@ -358,6 +359,7 @@ variable (c : Basis o R₂ M₂') variable [DecidableEq o] +set_option maxHeartbeats 1600000 in -- Cannot be a `simp` lemma because `b` must be inferred. theorem BilinForm.toMatrix_comp (B : BilinForm R₂ M₂) (l r : M₂' →ₗ[R₂] M₂) : BilinForm.toMatrix c (B.comp l r) = diff --git a/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean b/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean index 74a6c6c02351a..c8f686ede849b 100644 --- a/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean +++ b/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean @@ -279,6 +279,7 @@ variable [Fintype n'] [Fintype m'] variable [DecidableEq n'] [DecidableEq m'] +set_option maxHeartbeats 400000 in @[simp] theorem LinearMap.toMatrix₂'_compl₁₂ (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (l : (n' → R) →ₗ[R] n → R) (r : (m' → R) →ₗ[R] m → R) : @@ -438,6 +439,7 @@ variable [Fintype n'] [Fintype m'] variable [DecidableEq n'] [DecidableEq m'] +set_option maxHeartbeats 3200000 in -- Cannot be a `simp` lemma because `b₁` and `b₂` must be inferred. theorem LinearMap.toMatrix₂_compl₁₂ (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (l : M₁' →ₗ[R] M₁) (r : M₂' →ₗ[R] M₂) : diff --git a/Mathlib/RepresentationTheory/Character.lean b/Mathlib/RepresentationTheory/Character.lean index e95ca1b76f1da..ccc5b71e04d3d 100644 --- a/Mathlib/RepresentationTheory/Character.lean +++ b/Mathlib/RepresentationTheory/Character.lean @@ -44,6 +44,7 @@ def character (V : FdRep k G) (g : G) := LinearMap.trace k V (V.ρ g) #align fdRep.character FdRep.character +set_option maxHeartbeats 1600000 in theorem char_mul_comm (V : FdRep k G) (g : G) (h : G) : V.character (h * g) = V.character (g * h) := by simp only [trace_mul_comm, character, map_mul] #align fdRep.char_mul_comm FdRep.char_mul_comm diff --git a/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean b/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean index c2e8043a3b16c..b8ad8f6299f8f 100644 --- a/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean +++ b/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean @@ -99,6 +99,7 @@ namespace inhomogeneousCochains open Rep groupCohomology +set_option maxHeartbeats 400000 in /-- The differential in the complex of inhomogeneous cochains used to calculate group cohomology. -/ @[simps] diff --git a/Mathlib/RingTheory/Kaehler.lean b/Mathlib/RingTheory/Kaehler.lean index 1e34ef46ad200..686a320f15595 100644 --- a/Mathlib/RingTheory/Kaehler.lean +++ b/Mathlib/RingTheory/Kaehler.lean @@ -268,7 +268,7 @@ def Derivation.liftKaehlerDifferential (D : Derivation R S M) : Ω[S⁄R] →ₗ refine Submodule.smul_induction_on hx ?_ ?_ · rintro x (hx : _ = _) y - dsimp - rw [show ↑(x • y) = x * ↑y by rfl, Derivation.tensorProductTo_mul, hx, y.prop, zero_smul, + rw [Derivation.tensorProductTo_mul, hx, y.prop, zero_smul, zero_smul, zero_add] · intro x y ex ey; rw [map_add, ex, ey, zero_add] #align derivation.lift_kaehler_differential Derivation.liftKaehlerDifferential diff --git a/Mathlib/RingTheory/PowerSeries/Basic.lean b/Mathlib/RingTheory/PowerSeries/Basic.lean index b37b2f078bd9e..3cc3f0e40f0b8 100644 --- a/Mathlib/RingTheory/PowerSeries/Basic.lean +++ b/Mathlib/RingTheory/PowerSeries/Basic.lean @@ -335,6 +335,7 @@ instance : Semiring (MvPowerSeries σ R) := end Semiring +set_option maxHeartbeats 300000 in instance [CommSemiring R] : CommSemiring (MvPowerSeries σ R) := { show Semiring (MvPowerSeries σ R) by infer_instance with mul_comm := fun φ ψ => From de3e6c195153ee1b676a6c78e51574ac21ea6500 Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Wed, 13 Dec 2023 13:48:45 -0500 Subject: [PATCH 7/9] timeout --- Mathlib/Algebra/Lie/Killing.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Algebra/Lie/Killing.lean b/Mathlib/Algebra/Lie/Killing.lean index 203338231ddf1..fb51d0e86aea5 100644 --- a/Mathlib/Algebra/Lie/Killing.lean +++ b/Mathlib/Algebra/Lie/Killing.lean @@ -207,6 +207,7 @@ lemma eq_zero_of_mem_weightSpace_mem_posFitting [LieAlgebra.IsNilpotent R L] obtain ⟨m, rfl⟩ := (mem_posFittingCompOf R x m₁).mp hm₁ k simp [hB, hk] +set_option maxHeartbeats 1600000 in lemma trace_toEndomorphism_eq_zero_of_mem_lcs {k : ℕ} {x : L} (hk : 1 ≤ k) (hx : x ∈ lowerCentralSeries R L L k) : trace R _ (toEndomorphism R L M x) = 0 := by From ca5cf2966695d198b0fe4bb0228040cc8748a09e Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Wed, 13 Dec 2023 14:00:48 -0500 Subject: [PATCH 8/9] lint --- Mathlib/Algebra/Ring/Equiv.lean | 1 - Mathlib/Algebra/Ring/Hom/Defs.lean | 1 - 2 files changed, 2 deletions(-) diff --git a/Mathlib/Algebra/Ring/Equiv.lean b/Mathlib/Algebra/Ring/Equiv.lean index 6b4fc70930171..aaad75a211b28 100644 --- a/Mathlib/Algebra/Ring/Equiv.lean +++ b/Mathlib/Algebra/Ring/Equiv.lean @@ -746,7 +746,6 @@ theorem toRingHom_refl : (RingEquiv.refl R).toRingHom = RingHom.id R := rfl #align ring_equiv.to_ring_hom_refl RingEquiv.toRingHom_refl -@[simp] theorem toMonoidHom_refl : (RingEquiv.refl R).toMonoidHom = MonoidHom.id R := rfl #align ring_equiv.to_monoid_hom_refl RingEquiv.toMonoidHom_refl diff --git a/Mathlib/Algebra/Ring/Hom/Defs.lean b/Mathlib/Algebra/Ring/Hom/Defs.lean index 2c06293b3a45a..04f3504fdd814 100644 --- a/Mathlib/Algebra/Ring/Hom/Defs.lean +++ b/Mathlib/Algebra/Ring/Hom/Defs.lean @@ -646,7 +646,6 @@ theorem coe_addMonoidHom_id : (id α : α →+ α) = AddMonoidHom.id α := rfl #align ring_hom.coe_add_monoid_hom_id RingHom.coe_addMonoidHom_id -@[simp] theorem coe_monoidHom_id : (id α : α →* α) = MonoidHom.id α := rfl #align ring_hom.coe_monoid_hom_id RingHom.coe_monoidHom_id From 20c3ea41ce0a1a334fecc7c0379ea4e3653d3cb2 Mon Sep 17 00:00:00 2001 From: Matthew Ballard Date: Wed, 13 Dec 2023 15:40:54 -0500 Subject: [PATCH 9/9] rm --- Mathlib/Algebra/Algebra/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean index 513aa1fd4bf59..3c4822bd37fb6 100644 --- a/Mathlib/Algebra/Algebra/Basic.lean +++ b/Mathlib/Algebra/Algebra/Basic.lean @@ -432,7 +432,7 @@ theorem coe_linearMap : ⇑(Algebra.linearMap R A) = algebraMap R A := rfl #align algebra.coe_linear_map Algebra.coe_linearMap -@[reducible] instance id : Algebra R R := +instance id : Algebra R R := (RingHom.id R).toAlgebra #align algebra.id Algebra.id