From e73c5b8cdc896a187aafed300f0721880aaa3e26 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Sun, 19 Apr 2026 20:17:37 +0200 Subject: [PATCH 1/3] fix --- Mathlib/Algebra/Lie/Ideal.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Lie/Ideal.lean b/Mathlib/Algebra/Lie/Ideal.lean index c7bdf292d59f00..dfc2cf6837f50f 100644 --- a/Mathlib/Algebra/Lie/Ideal.lean +++ b/Mathlib/Algebra/Lie/Ideal.lean @@ -73,17 +73,18 @@ theorem LieIdeal.toLieSubalgebra_toSubmodule (I : LieIdeal R L) : rfl /-- An ideal of `L` is a Lie subalgebra of `L`, so it is a Lie ring. -/ -instance LieIdeal.lieRing (I : LieIdeal R L) : LieRing I := - inferInstanceAs <| LieRing I.toLieSubalgebra +instance LieIdeal.lieRing (I : LieIdeal R L) : LieRing I where + bracket x y := ⟨⁅(x : L), y⁆, lie_mem_right R L I x y y.2⟩ + __ : LieRing I := inferInstanceAs <| LieRing I.toLieSubalgebra /-- Transfer the `LieAlgebra` instance from the coercion `LieIdeal → LieSubalgebra`. -/ instance LieIdeal.lieAlgebra (I : LieIdeal R L) : LieAlgebra R I := - inferInstanceAs <| LieAlgebra R I.toLieSubalgebra + fast_instance% show LieAlgebra R I.toLieSubalgebra from inferInstance /-- Transfer the `LieRingModule` instance from the coercion `LieIdeal → LieSubalgebra`. -/ instance LieIdeal.lieRingModule {R L : Type*} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieRingModule L M] : LieRingModule I M := - inferInstanceAs <| LieRingModule I.toLieSubalgebra M + fast_instance% show LieRingModule I.toLieSubalgebra M from inferInstance @[simp] theorem LieIdeal.coe_bracket_of_module {R L : Type*} [CommRing R] [LieRing L] [LieAlgebra R L] From e706bd110f3a3fc85422b2cdd06bf7674a52f3a2 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Mon, 20 Apr 2026 14:32:55 +0200 Subject: [PATCH 2/3] better, no fast_instance --- Mathlib/Algebra/Lie/Ideal.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Lie/Ideal.lean b/Mathlib/Algebra/Lie/Ideal.lean index dfc2cf6837f50f..9b3dbef4e2d4cb 100644 --- a/Mathlib/Algebra/Lie/Ideal.lean +++ b/Mathlib/Algebra/Lie/Ideal.lean @@ -79,12 +79,16 @@ instance LieIdeal.lieRing (I : LieIdeal R L) : LieRing I where /-- Transfer the `LieAlgebra` instance from the coercion `LieIdeal → LieSubalgebra`. -/ instance LieIdeal.lieAlgebra (I : LieIdeal R L) : LieAlgebra R I := - fast_instance% show LieAlgebra R I.toLieSubalgebra from inferInstance + inferInstanceAs <| LieAlgebra R I.toLieSubalgebra + +instance LieIdeal.bracket {R L : Type*} [CommRing R] [LieRing L] [LieAlgebra R L] + (I : LieIdeal R L) [Bracket L M] : Bracket I M where + bracket x m := ⁅(x : L), m⁆ /-- Transfer the `LieRingModule` instance from the coercion `LieIdeal → LieSubalgebra`. -/ instance LieIdeal.lieRingModule {R L : Type*} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieRingModule L M] : LieRingModule I M := - fast_instance% show LieRingModule I.toLieSubalgebra M from inferInstance + inferInstanceAs <| LieRingModule I.toLieSubalgebra M @[simp] theorem LieIdeal.coe_bracket_of_module {R L : Type*} [CommRing R] [LieRing L] [LieAlgebra R L] From d57e9ef36ba961fd731d00a69d71b6800ca4d545 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Mon, 20 Apr 2026 17:11:19 +0200 Subject: [PATCH 3/3] move up --- Mathlib/Algebra/Lie/Ideal.lean | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/Mathlib/Algebra/Lie/Ideal.lean b/Mathlib/Algebra/Lie/Ideal.lean index 9b3dbef4e2d4cb..6fd2210fcd1161 100644 --- a/Mathlib/Algebra/Lie/Ideal.lean +++ b/Mathlib/Algebra/Lie/Ideal.lean @@ -72,19 +72,20 @@ theorem LieIdeal.toLieSubalgebra_toSubmodule (I : LieIdeal R L) : ((I : LieSubalgebra R L) : Submodule R L) = LieSubmodule.toSubmodule I := rfl +instance LieIdeal.bracket {R L : Type*} [CommRing R] [LieRing L] [LieAlgebra R L] + (I : LieIdeal R L) [Bracket L M] : Bracket I M where + bracket x m := ⁅(x : L), m⁆ + +instance (priority := 2000) (I : LieIdeal R L) : Bracket I I := inferInstance + /-- An ideal of `L` is a Lie subalgebra of `L`, so it is a Lie ring. -/ -instance LieIdeal.lieRing (I : LieIdeal R L) : LieRing I where - bracket x y := ⟨⁅(x : L), y⁆, lie_mem_right R L I x y y.2⟩ - __ : LieRing I := inferInstanceAs <| LieRing I.toLieSubalgebra +instance LieIdeal.lieRing (I : LieIdeal R L) : LieRing I := + inferInstanceAs <| LieRing I.toLieSubalgebra /-- Transfer the `LieAlgebra` instance from the coercion `LieIdeal → LieSubalgebra`. -/ instance LieIdeal.lieAlgebra (I : LieIdeal R L) : LieAlgebra R I := inferInstanceAs <| LieAlgebra R I.toLieSubalgebra -instance LieIdeal.bracket {R L : Type*} [CommRing R] [LieRing L] [LieAlgebra R L] - (I : LieIdeal R L) [Bracket L M] : Bracket I M where - bracket x m := ⁅(x : L), m⁆ - /-- Transfer the `LieRingModule` instance from the coercion `LieIdeal → LieSubalgebra`. -/ instance LieIdeal.lieRingModule {R L : Type*} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieRingModule L M] : LieRingModule I M :=