awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz :
  Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1) (1 ⊗ₜ[R] z)
⊢ Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (LieAlgebra.center A (A ⊗[R] L)) (1 ⊗ₜ[R] z)

Tactic:
replace hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L) := by
    simp only [mem_maxTrivSubmodule] at hzc ⊢
    intro y
    exact y.induction_on rfl (fun a u ↦ by simp [hzc u])
      (fun u v hu hv ↦ by simp [A, hu, hv])
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz :
  Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1) (1 ⊗ₜ[R] z)
hzc : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (LieAlgebra.center A (A ⊗[R] L)) (1 ⊗ₜ[R] z)
h :
  Eq (α := Submodule A (A ⊗[R] M))
    (⨆ (μ : A),
      End.maxGenEigenspace ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x)) μ)
    ⊤
h₁ :
  ∀ (μ : A),
    Eq.{u_1 + 1} (α := A)
      ((trace A
              ↥(End.maxGenEigenspace ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x))
                  μ) :
            (a :
                ↥(((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x)).maxGenEigenspace
                      μ) →ₗ[A]
                  ↥(((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x)).maxGenEigenspace
                      μ)) →
              A)
          (LinearMap.restrict ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] z)) ⋯) :
        A)
      (0 : A)
h₂ :
  Commute (S := End A (A ⊗[R] M))
    ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x) : End A (A ⊗[R] M))
    ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] z) : End A (A ⊗[R] M))
⊢ Eq.{u_1 + 1} (α := A)
    ((trace A (A ⊗[R] M) : (a : A ⊗[R] M →ₗ[A] A ⊗[R] M) → A)
        ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] z) ∘ₗ
          (toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x)) :
      A)
    (0 : A)

Tactic:
apply LinearMap.trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero

Premises used: LinearMap.trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz :
  Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1) (1 ⊗ₜ[R] z)
hzc : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (LieAlgebra.center A (A ⊗[R] L)) (1 ⊗ₜ[R] z)
⊢ Eq (α := Submodule A (A ⊗[R] M))
    (⨆ (μ : A),
      End.maxGenEigenspace ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x)) μ)
    ⊤

Tactic:
IsTriangularizable.maxGenEigenspace_eq_top (1 ⊗ₜ[R] x)

Premises used: LieModule.IsTriangularizable.maxGenEigenspace_eq_top, TensorProduct.tmul, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz :
  Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1) (1 ⊗ₜ[R] z)
hzc : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (LieAlgebra.center A (A ⊗[R] L)) (1 ⊗ₜ[R] z)
⊢ Eq (α := Submodule A (A ⊗[R] M))
    (⨆ (μ : A),
      End.maxGenEigenspace ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x)) μ)
    ⊤

Tactic:
exact IsTriangularizable.maxGenEigenspace_eq_top (1 ⊗ₜ[R] x)

Premises used: LieModule.IsTriangularizable.maxGenEigenspace_eq_top, TensorProduct.tmul, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz :
  Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1) (1 ⊗ₜ[R] z)
hzc : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (LieAlgebra.center A (A ⊗[R] L)) (1 ⊗ₜ[R] z)
⊢ ∀ (μ : A),
    Eq.{u_1 + 1} (α := A)
      ((trace A
              ↥(End.maxGenEigenspace ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x))
                  μ) :
            (a :
                ↥(((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x)).maxGenEigenspace
                      μ) →ₗ[A]
                  ↥(((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x)).maxGenEigenspace
                      μ)) →
              A)
          (LinearMap.restrict ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] z)) ⋯) :
        A)
      (0 : A)

Tactic:
fun μ ↦ trace_toEnd_eq_zero_of_mem_lcs A (A ⊗[R] L)
      (genWeightSpaceOf (A ⊗[R] M) μ ((1 : A) ⊗ₜ[R] x)) (le_refl 1) hz

Premises used: LieModule.trace_toEnd_eq_zero_of_mem_lcs, le_refl, LieModule.genWeightSpaceOf, Quotient.liftOn', Set.Mem, iSup, AddCon.liftOn, setOf, Membership.mem, Subtype, LinearMap.restrict, LinearMap.codRestrict, TensorProduct, TensorProduct.tmul, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz :
  Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1) (1 ⊗ₜ[R] z)
hzc : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (LieAlgebra.center A (A ⊗[R] L)) (1 ⊗ₜ[R] z)
⊢ ∀ (μ : A),
    Eq.{u_1 + 1} (α := A)
      ((trace A
              ↥(End.maxGenEigenspace ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x))
                  μ) :
            (a :
                ↥(((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x)).maxGenEigenspace
                      μ) →ₗ[A]
                  ↥(((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x)).maxGenEigenspace
                      μ)) →
              A)
          (LinearMap.restrict ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] z)) ⋯) :
        A)
      (0 : A)

Tactic:
exact fun μ ↦ trace_toEnd_eq_zero_of_mem_lcs A (A ⊗[R] L)
      (genWeightSpaceOf (A ⊗[R] M) μ ((1 : A) ⊗ₜ[R] x)) (le_refl 1) hz

Premises used: LieModule.trace_toEnd_eq_zero_of_mem_lcs, le_refl, LieModule.genWeightSpaceOf, Membership.mem, Subtype, TensorProduct, TensorProduct.tmul, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz :
  Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1) (1 ⊗ₜ[R] z)
hzc : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (LieAlgebra.center A (A ⊗[R] L)) (1 ⊗ₜ[R] z)
⊢ Commute (S := End A (A ⊗[R] M))
    ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x) : End A (A ⊗[R] M))
    ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] z) : End A (A ⊗[R] M))

Tactic:
commute_toEnd_of_mem_center_right (A ⊗[R] M) hzc (1 ⊗ₜ x)

Premises used: LieModule.commute_toEnd_of_mem_center_right, TensorProduct, TensorProduct.tmul, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz :
  Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1) (1 ⊗ₜ[R] z)
hzc : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (LieAlgebra.center A (A ⊗[R] L)) (1 ⊗ₜ[R] z)
⊢ Commute (S := End A (A ⊗[R] M))
    ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x) : End A (A ⊗[R] M))
    ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] z) : End A (A ⊗[R] M))

Tactic:
exact commute_toEnd_of_mem_center_right (A ⊗[R] M) hzc (1 ⊗ₜ x)

Premises used: LieModule.commute_toEnd_of_mem_center_right, TensorProduct, TensorProduct.tmul, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
h : Eq (α := Submodule R L) (LinearMap.ker (traceForm R L M)) ⊥
⊢ IsLieAbelian L

Tactic:
simpa only [← disjoint_lowerCentralSeries_maxTrivSubmodule_iff R L L, disjoint_iff_inf_le,
    LieIdeal.toLieSubalgebra_toSubmodule, LieSubmodule.toSubmodule_eq_bot, h]
    using lowerCentralSeries_one_inf_center_le_ker_traceForm R L M

Premises used: LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm, LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iff, LieIdeal.toLieSubalgebra_toSubmodule, disjoint_iff_inf_le, LieSubmodule.toSubmodule_eq_bot
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Free R M
inst_8 : Module.Finite R M
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
hy' :
  ∀ m ∈ N,
    Membership.mem (α := M) N
      ((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
              ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y :
            (a : M) → M)
          m :
        M)
this : ∀ (m : M), ⁅x, ⁅y, m⁆⁆ ∈ N
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R ↥N : (a : ↥N →ₗ[R] ↥N) → R)
        (LinearMap.restrict
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y)
          ⋯) :
      R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
      R)

Tactic:
have : (trace R { x // x ∈ N }) ((φ x ∘ₗ φ y).restrict _) = (trace R M) (φ x ∘ₗ φ y) :=
      (φ x ∘ₗ φ y).trace_restrict_eq_of_forall_mem _ this
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Free R M
inst_8 : Module.Finite R M
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
hy' :
  ∀ m ∈ N,
    Membership.mem (α := M) N
      ((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
              ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y :
            (a : M) → M)
          m :
        M)
this_1 : ∀ (m : M), ⁅x, ⁅y, m⁆⁆ ∈ N
this :
  Eq.{u_1 + 1} (α := R)
    ((trace R ↥N : (a : ↥N →ₗ[R] ↥N) → R)
        (LinearMap.restrict
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y)
          ⋯) :
      R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
      R)
    ((trace R ↥N : (a : ↥N →ₗ[R] ↥N) → R)
        (LinearMap.restrict
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y)
          hy') :
      R)

Tactic:
simp [this]
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Free R M
inst_8 : Module.Finite R M
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
hy' :
  ∀ m ∈ N,
    Membership.mem (α := M) N
      ((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
              ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y :
            (a : M) → M)
          m :
        M)
suffices : ∀ (m : M), ⁅x, ⁅y, m⁆⁆ ∈ N
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
      R)
    ((trace R ↥N : (a : ↥N →ₗ[R] ↥N) → R)
        (LinearMap.restrict
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y)
          hy') :
      R)

Tactic:
suffices ∀ m, ⁅x, ⁅y, m⁆⁆ ∈ N by
    have : (trace R { x // x ∈ N }) ((φ x ∘ₗ φ y).restrict _) = (trace R M) (φ x ∘ₗ φ y) :=
      (φ x ∘ₗ φ y).trace_restrict_eq_of_forall_mem _ this
    simp [this]
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Free R M
inst_8 : Module.Finite R M
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
hy' :
  ∀ m ∈ N,
    Membership.mem (α := M) N
      ((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
              ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y :
            (a : M) → M)
          m :
        M)
⊢ ∀ (m : M), ⁅x, ⁅y, m⁆⁆ ∈ N

Tactic:
fun m ↦ N.lie_mem (h hy m)

Premises used: Set.Mem, LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Free R M
inst_8 : Module.Finite R M
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
hy' :
  ∀ m ∈ N,
    Membership.mem (α := M) N
      ((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
              ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y :
            (a : M) → M)
          m :
        M)
⊢ ∀ (m : M), ⁅x, ⁅y, m⁆⁆ ∈ N

Tactic:
exact fun m ↦ N.lie_mem (h hy m)

Premises used: LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Free R M
inst_8 : Module.Finite R M
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
H :
  ∀ (x : L) (hx : x ∈ I) (y : L) (hy : y ∈ I),
    Eq.{u_1 + 1} (α := R)
      ((((traceForm.{u_1, u_3, u_4} R ↥I ↥N : (a : ↥I) → ↥I →ₗ[R] R) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) :
              LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (↥I) R) :
            (a : ↥I) → R)
          (Subtype.mk (p := fun (x : L) ↦ x ∈ I) y hy) :
        R)
      ((((LinearMap.BilinForm.restrict (traceForm R L M) (LieIdeal.toLieSubalgebra R L I).toSubmodule :
                  (a : ↥I) → ↥I →ₗ[R] R)
                (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) :
              LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (↥I) R) :
            (a : ↥I) → R)
          (Subtype.mk (p := fun (x : L) ↦ x ∈ I) y hy) :
        R)
⊢ traceForm.{u_1, u_3, u_4} R ↥I ↥N =
    LinearMap.BilinForm.restrict (traceForm R L M) (LieIdeal.toLieSubalgebra R L I).toSubmodule

Tactic:
ext ⟨x, hx⟩ ⟨y, hy⟩
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Free R M
inst_8 : Module.Finite R M
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x : L
hx : x ∈ I
y : L
hy : y ∈ I
H :
  Eq.{u_1 + 1} (α := R)
    ((((traceForm.{u_1, u_3, u_4} R ↥I ↥N : (a : ↥I) → ↥I →ₗ[R] R) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) :
            LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (↥I) R) :
          (a : ↥I) → R)
        (Subtype.mk (p := fun (x : L) ↦ x ∈ I) y hy) :
      R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((traceForm.{u_1, u_3, u_4} R ↥I ↥N : (a : ↥I) → ↥I →ₗ[R] R) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) :
            LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (↥I) R) :
          (a : ↥I) → R)
        (Subtype.mk (p := fun (x : L) ↦ x ∈ I) y hy) :
      R)
    ((((LinearMap.BilinForm.restrict (traceForm R L M) (LieIdeal.toLieSubalgebra R L I).toSubmodule :
                (a : ↥I) → ↥I →ₗ[R] R)
              (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) :
            LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (↥I) R) :
          (a : ↥I) → R)
        (Subtype.mk (p := fun (x : L) ↦ x ∈ I) y hy) :
      R)

Tactic:
change _ = trace R M (φ x ∘ₗ φ y)
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Free R M
inst_8 : Module.Finite R M
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x : L
hx : x ∈ I
y : L
hy : y ∈ I
H :
  Eq.{u_1 + 1} (α := R)
    ((((traceForm.{u_1, u_3, u_4} R ↥I ↥N : (a : ↥I) → ↥I →ₗ[R] R) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) :
            LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (↥I) R) :
          (a : ↥I) → R)
        (Subtype.mk (p := fun (x : L) ↦ x ∈ I) y hy) :
      R)
    ((trace R ↥N : (a : ↥N →ₗ[R] ↥N) → R)
        (LinearMap.restrict
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y)
          ⋯) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((traceForm.{u_1, u_3, u_4} R ↥I ↥N : (a : ↥I) → ↥I →ₗ[R] R) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) :
            LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (↥I) R) :
          (a : ↥I) → R)
        (Subtype.mk (p := fun (x : L) ↦ x ∈ I) y hy) :
      R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
      R)

Tactic:
rw [N.trace_eq_trace_restrict_of_le_idealizer I h x hy]

Premises used: LieSubmodule.trace_eq_trace_restrict_of_le_idealizer, LieSubmodule.lie_mem, LieSubmodule.mem_idealizer, Iff.mp
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Free R M
inst_8 : Module.Finite R M
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x : L
hx : x ∈ I
y : L
hy : y ∈ I
⊢ Eq.{u_1 + 1} (α := R)
    ((((traceForm.{u_1, u_3, u_4} R ↥I ↥N : (a : ↥I) → ↥I →ₗ[R] R) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) :
            LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (↥I) R) :
          (a : ↥I) → R)
        (Subtype.mk (p := fun (x : L) ↦ x ∈ I) y hy) :
      R)
    ((trace R ↥N : (a : ↥N →ₗ[R] ↥N) → R)
        (LinearMap.restrict
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y)
          ⋯) :
      R)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Free R M
inst_8 : Module.Finite R M
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
N : LieSubmodule R L M
I : LieIdeal R L
h : I ≤ N.idealizer
x y : L
hy : y ∈ I
inst_11 : LieModule.IsTrivial.{u_3, u_4} ↥I ↥N
hy' : ∀ m ∈ N,
  Membership.mem (α := M) N
    ((((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y :
          (a : M) → M)
        m :
      M) :=
  ⋯
this :
  LinearMap.restrict
      (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
        ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y)
      hy' =
    0
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
      R)
    (0 : R)

Tactic:
simp [this, N.trace_eq_trace_restrict_of_le_idealizer I h x hy]

Premises used: LieSubmodule.trace_eq_trace_restrict_of_le_idealizer, LieSubmodule.lie_mem, LieSubmodule.mem_idealizer, Iff.mp