awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Quotient
Goal:
R : Type u_1
L : Type u_2
L' : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
y : L ⧸ f.ker
z : L
H :
  ∀ (z_1 : L),
    Eq.{u_3 + 1} (α := ↥f.range)
      (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
          (Bracket.bracket (L := L ⧸ f.ker) (Submodule.Quotient.mk z) (Submodule.Quotient.mk z_1)) :
        ↥(↑f : L →ₗ[R] L').range)
      (Bracket.bracket (L := ↥f.range)
          (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
              (Submodule.Quotient.mk z) :
            ↥(↑f : L →ₗ[R] L').range)
          (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
            (Submodule.Quotient.mk z_1)) :
        ↥f.range)
⊢ Eq.{u_3 + 1} (α := ↥f.range)
    (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
        (Bracket.bracket (L := L ⧸ f.ker) (Submodule.Quotient.mk z) y) :
      ↥(↑f : L →ₗ[R] L').range)
    (Bracket.bracket (L := ↥f.range)
        (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
            (Submodule.Quotient.mk z) :
          ↥(↑f : L →ₗ[R] L').range)
        (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range) y) :
      ↥f.range)

Tactic:
induction y using Submodule.Quotient.induction_on
-- Module: Mathlib.Algebra.Lie.Quotient
Goal:
R : Type u_1
L : Type u_2
L' : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
z z_1 : L
H :
  Eq.{u_3 + 1} (α := L')
    (↑(((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
          (Bracket.bracket (L := L ⧸ f.ker) (Submodule.Quotient.mk z) (Submodule.Quotient.mk z_1))) :
      L')
    (Bracket.bracket (L := L')
      (↑(((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
            (Submodule.Quotient.mk z)) :
        L')
      (↑(((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
            (Submodule.Quotient.mk z_1)) :
        L'))
⊢ Eq.{u_3 + 1} (α := ↥f.range)
    (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
        (Bracket.bracket (L := L ⧸ f.ker) (Submodule.Quotient.mk z) (Submodule.Quotient.mk z_1)) :
      ↥(↑f : L →ₗ[R] L').range)
    (Bracket.bracket (L := ↥f.range)
        (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
            (Submodule.Quotient.mk z) :
          ↥(↑f : L →ₗ[R] L').range)
        (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
          (Submodule.Quotient.mk z_1)) :
      ↥f.range)

Tactic:
rw [← SetLike.coe_eq_coe, LieSubalgebra.coe_bracket f.range]

Premises used: SetLike.coe_eq_coe, LieHom.range, LieSubalgebra.coe_bracket
-- Module: Mathlib.Algebra.Lie.Quotient
Goal:
R : Type u_1
L : Type u_2
L' : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
z z_1 : L
⊢ Eq.{u_3 + 1} (α := L')
    (↑(((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
          (Bracket.bracket (L := L ⧸ f.ker) (Submodule.Quotient.mk z) (Submodule.Quotient.mk z_1))) :
      L')
    (Bracket.bracket (L := L')
      (↑(((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
            (Submodule.Quotient.mk z)) :
        L')
      (↑(((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
            (Submodule.Quotient.mk z_1)) :
        L'))

Tactic:
simp only [← LieSubmodule.Quotient.mk_bracket, LinearMap.quotKerEquivRange_apply_mk,
        coe_toLinearMap, map_lie]

Premises used: LieHom.map_lie, LinearMap.quotKerEquivRange_apply_mk, LieHom.coe_toLinearMap, LieSubmodule.Quotient.mk_bracket
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
ι : Type u_5
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : Free R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
inst_9 : Module.Finite R M
inst_10 : Free R M
inst_11 : Fintype ι
b : Basis ι R L
inst_12 : Nontrivial R
inst_13 : DecidableEq ι
⊢ (polyCharpoly (↑(toEnd R L M) : L →ₗ[R] End R M) b).coeff (rank R L M) ≠ 0

Tactic:
polyCharpoly_coeff_nilRank_ne_zero _ _

Premises used: LieModule.rank, LinearMap.polyCharpoly_coeff_nilRank_ne_zero
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
ι : Type u_5
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : Free R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
inst_9 : Module.Finite R M
inst_10 : Free R M
inst_11 : Fintype ι
b : Basis ι R L
inst_12 : Nontrivial R
inst_13 : DecidableEq ι
⊢ rank R L M = (polyCharpoly (↑(toEnd R L M) : L →ₗ[R] End R M) b).natTrailingDegree

Tactic:
apply nilRank_eq_polyCharpoly_natTrailingDegree

Premises used: LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
ιₘ : Type u_6
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : Free R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
inst_9 : Module.Finite R M
inst_10 : Free R M
inst_11 : Fintype ιₘ
bₘ : Basis ιₘ R M
inst_12 : Nontrivial R
⊢ rank R L M ≤ Fintype.card ιₘ

Tactic:
nilRank_le_card _ bₘ

Premises used: LieModule.rank, LinearMap.nilRank_le_card
-- Module: Mathlib.Algebra.Lie.Rank
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 : Module.Finite R L
inst_4 : Free R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
inst_9 : Module.Finite R M
inst_10 : Free R M
inst_11 : Nontrivial R
⊢ rank R L M ≤ finrank R M

Tactic:
nilRank_le_finrank _

Premises used: LieModule.rank, LinearMap.nilRank_le_finrank
-- Module: Mathlib.Algebra.Lie.Rank
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 : Module.Finite R L
inst_4 : Free R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
inst_9 : Module.Finite R M
inst_10 : Free R M
x : L
inst_11 : Nontrivial R
⊢ rank R L M ≤
    Polynomial.natTrailingDegree.{u_1} (R := R)
      (charpoly.{u_1, u_4} (M := M) (((toEnd R L M : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x))

Tactic:
nilRank_le_natTrailingDegree_charpoly _ _

Premises used: LieModule.rank, LinearMap.nilRank_le_natTrailingDegree_charpoly
-- Module: Mathlib.Algebra.Lie.Rank
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 : Module.Finite R L
inst_4 : Free R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
inst_9 : Module.Finite R M
inst_10 : Free R M
x : L
⊢ IsRegular R M x ↔
    Ne.{u_1 + 1} (α := R)
      (Polynomial.coeff
        (charpoly.{u_1, u_4} (M := M) (((toEnd R L M : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x))
        (rank R L M))
      0

Tactic:
Iff.rfl

Premises used: LieModule.rank, LieModule.IsRegular, Iff.rfl, LinearMap.IsNilRegular
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
ι : Type u_5
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : Free R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
inst_9 : Module.Finite R M
inst_10 : Free R M
inst_11 : Fintype ι
b : Basis ι R L
x : L
inst_12 : DecidableEq ι
⊢ IsRegular R M x ↔
    Ne.{u_1 + 1} (α := R)
      ((MvPolynomial.eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
          ((polyCharpoly (↑(toEnd R L M) : L →ₗ[R] End R M) b).coeff (rank R L M)) :
        R)
      (0 : R)

Tactic:
LinearMap.isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero _ _ _

Premises used: LieModule.rank, LieModule.IsRegular, LinearMap.isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero
-- Module: Mathlib.Algebra.Lie.Rank
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 : Module.Finite R L
inst_4 : Free R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
inst_9 : Module.Finite R M
inst_10 : Free R M
x : L
inst_11 : Nontrivial R
⊢ IsRegular R M x ↔
    Polynomial.natTrailingDegree.{u_1} (R := R)
        (charpoly.{u_1, u_4} (M := M) (((toEnd R L M : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x)) =
      rank R L M

Tactic:
LinearMap.isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank _ _

Premises used: LieModule.rank, LinearMap.isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank, LieModule.IsRegular
-- Module: Mathlib.Algebra.Lie.Rank
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 : Module.Finite R L
inst_4 : Free R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
inst_9 : Module.Finite R M
inst_10 : Free R M
inst_11 : IsDomain R
h : (↑(finrank R M) : Cardinal.{u_1}) ≤ #R
⊢ ∃ (x : L), IsRegular R M x

Tactic:
LinearMap.exists_isNilRegular_of_finrank_le_card _ h

Premises used: LieModule.IsRegular, LinearMap.exists_isNilRegular_of_finrank_le_card
-- Module: Mathlib.Algebra.Lie.Rank
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 : Module.Finite R L
inst_4 : Free R L
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : LieRingModule L M
inst_8 : LieModule R L M
inst_9 : Module.Finite R M
inst_10 : Free R M
inst_11 : IsDomain R
inst_12 : Infinite R
⊢ ∃ (x : L), IsRegular R M x

Tactic:
LinearMap.exists_isNilRegular _

Premises used: LieModule.IsRegular, LinearMap.exists_isNilRegular
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
R : Type u_1
L : Type u_3
ι : Type u_5
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : Free R L
inst_5 : Fintype ι
b : Basis ι R L
inst_6 : Nontrivial R
inst_7 : DecidableEq ι
⊢ (polyCharpoly (↑(ad R L) : L →ₗ[R] End R L) b).coeff (rank R L) ≠ 0

Tactic:
polyCharpoly_coeff_nilRank_ne_zero _ _

Premises used: LieModule.rank, LinearMap.polyCharpoly_coeff_nilRank_ne_zero
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
R : Type u_1
L : Type u_3
ι : Type u_5
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : Free R L
inst_5 : Fintype ι
b : Basis ι R L
inst_6 : Nontrivial R
inst_7 : DecidableEq ι
⊢ rank R L = (polyCharpoly (↑(ad R L) : L →ₗ[R] End R L) b).natTrailingDegree

Tactic:
apply nilRank_eq_polyCharpoly_natTrailingDegree

Premises used: LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
R : Type u_1
L : Type u_3
ι : Type u_5
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : Free R L
inst_5 : Fintype ι
b : Basis ι R L
inst_6 : Nontrivial R
⊢ rank R L ≤ Fintype.card ι

Tactic:
nilRank_le_card _ b

Premises used: LieModule.rank, LinearMap.nilRank_le_card
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : Free R L
inst_5 : Nontrivial R
⊢ rank R L ≤ finrank R L

Tactic:
nilRank_le_finrank _

Premises used: LieModule.rank, LinearMap.nilRank_le_finrank
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : Free R L
x : L
inst_5 : Nontrivial R
⊢ rank R L ≤ Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := L) ((ad R L : (a : L) → End R L) x))

Tactic:
nilRank_le_natTrailingDegree_charpoly _ _

Premises used: LieModule.rank, LinearMap.nilRank_le_natTrailingDegree_charpoly
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : Free R L
x : L
⊢ IsRegular R x ↔
    Ne.{u_1 + 1} (α := R) (Polynomial.coeff (charpoly.{u_1, u_3} (M := L) ((ad R L : (a : L) → End R L) x)) (rank R L))
      0

Tactic:
Iff.rfl

Premises used: LieModule.rank, LieModule.IsRegular, Iff.rfl, LinearMap.IsNilRegular
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
R : Type u_1
L : Type u_3
ι : Type u_5
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : Free R L
inst_5 : Fintype ι
b : Basis ι R L
x : L
inst_6 : DecidableEq ι
⊢ IsRegular R x ↔
    Ne.{u_1 + 1} (α := R)
      ((MvPolynomial.eval (⇑((b.repr : (a : L) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) : (a : MvPolynomial ι R) → R)
          ((polyCharpoly (↑(ad R L) : L →ₗ[R] End R L) b).coeff (rank R L)) :
        R)
      (0 : R)

Tactic:
LinearMap.isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero _ _ _

Premises used: LieModule.rank, LieModule.IsRegular, LinearMap.isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : Free R L
x : L
inst_5 : Nontrivial R
⊢ IsRegular R x ↔
    Polynomial.natTrailingDegree.{u_1} (R := R) (charpoly.{u_1, u_3} (M := L) ((ad R L : (a : L) → End R L) x)) =
      rank R L

Tactic:
LinearMap.isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank _ _

Premises used: LieModule.rank, LinearMap.isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank, LieModule.IsRegular
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : Free R L
inst_5 : IsDomain R
h : (↑(finrank R L) : Cardinal.{u_1}) ≤ #R
⊢ ∃ (x : L), IsRegular R x

Tactic:
LinearMap.exists_isNilRegular_of_finrank_le_card _ h

Premises used: LieModule.IsRegular, LinearMap.exists_isNilRegular_of_finrank_le_card
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : Free R L
inst_5 : IsDomain R
inst_6 : Infinite R
⊢ ∃ (x : L), IsRegular R x

Tactic:
LinearMap.exists_isNilRegular _

Premises used: LieModule.IsRegular, LinearMap.exists_isNilRegular
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
K : Type u_7
L : Type u_8
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
x : L
⊢ finrank.{u_7, u_8} K ↥(engel K x) =
    Polynomial.natTrailingDegree.{u_7} (R := K)
      (LinearMap.charpoly.{u_7, u_8} (M := L) ((ad K L : (a : L) → End K L) x))

Tactic:
(ad K L x).finrank_maxGenEigenspace_zero_eq

Premises used: Set.Mem, iSup, LieAlgebra.ad, setOf, LieSubalgebra.engel, LinearMap.finrank_maxGenEigenspace_zero_eq, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
K : Type u_7
L : Type u_8
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
x : L
⊢ rank K L ≤ finrank.{u_7, u_8} K ↥(engel K x)

Tactic:
(rank_le_natTrailingDegree_charpoly_ad K x).trans
    (finrank_engel K x).ge

Premises used: LieAlgebra.finrank_engel, Eq.ge, LieAlgebra.rank_le_natTrailingDegree_charpoly_ad, LE.le.trans
-- Module: Mathlib.Algebra.Lie.Rank
Goal:
K : Type u_7
L : Type u_8
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
x : L
rw :
  Polynomial.natTrailingDegree.{u_7} (R := K)
        (LinearMap.charpoly.{u_7, u_8} (M := L) ((ad K L : (a : L) → End K L) x)) =
      rank K L ↔
    finrank.{u_7, u_8} K ↥(engel K x) = rank K L
rw₁ rw₂ :
  Polynomial.natTrailingDegree.{u_7} (R := K)
        (LinearMap.charpoly.{u_7, u_8} (M := L) ((ad K L : (a : L) → End K L) x)) =
      rank K L ↔
    Polynomial.natTrailingDegree.{u_7} (R := K)
        (LinearMap.charpoly.{u_7, u_8} (M := L) ((ad K L : (a : L) → End K L) x)) =
      rank K L
⊢ IsRegular K x ↔ finrank.{u_7, u_8} K ↥(engel K x) = rank K L

Tactic:
rw [isRegular_iff_natTrailingDegree_charpoly_eq_rank, finrank_engel]

Premises used: LieAlgebra.finrank_engel, LieAlgebra.isRegular_iff_natTrailingDegree_charpoly_eq_rank
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : K ⋊⁅ψ⁆ L
⊢ (toProd : (a : K ⋊⁅ψ⁆ L) → K × L) x = (x.left, x.right)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : K ⋊⁅ψ⁆ L
⊢ Eq (α := K × L) ((toProdl ψ : (a : K ⋊⁅ψ⁆ L) → K × L) x : K × L) ((toProd : (a : K ⋊⁅ψ⁆ L) → K × L) x : K × L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
⊢ Eq (α := K ⋊⁅ψ⁆ L) 0 { left := 0, right := 0 }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x y : K ⋊⁅ψ⁆ L
⊢ x + y = { left := x.left + y.left, right := x.right + y.right }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x y : K ⋊⁅ψ⁆ L
⊢ x - y = { left := x.left - y.left, right := x.right - y.right }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : K ⋊⁅ψ⁆ L
⊢ -x = { left := -x.left, right := -x.right }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
t : R
x : K ⋊⁅ψ⁆ L
⊢ t • x = { left := t • x.left, right := t • x.right }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x y : K ⋊⁅ψ⁆ L
⊢ ⁅x, y⁆ =
    {
      left :=
        HSub.hSub (β := K)
          (HAdd.hAdd (β := K) ⁅x.left, y.left⁆
            ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) y.left : K))
          ((((ψ : (a : L) → LieDerivation R K K) y.right : LieDerivation R K K) : (a : K) → K) x.left : K),
      right := ⁅x.right, y.right⁆ }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x x_1 x_2 : K ⋊⁅ψ⁆ L
simp :
  ⁅x.left, x_2.left⁆ + ⁅x_1.left, x_2.left⁆ +
        HAdd.hAdd (α := K) (β := K)
          ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left : K)
          ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x_2.left : K) -
      HAdd.hAdd (α := K) (β := K)
        ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left : K)
        ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x_1.left : K) =
    HSub.hSub (β := K)
        (HAdd.hAdd (β := K) ⁅x.left, x_2.left⁆
          ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left : K))
        ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left : K) +
      HSub.hSub (β := K)
        (HAdd.hAdd (β := K) ⁅x_1.left, x_2.left⁆
          ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x_2.left : K))
        ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x_1.left : K)
⊢ ⁅x + x_1, x_2⁆ = ⁅x, x_2⁆ + ⁅x_1, x_2⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x x_1 x_2 : K ⋊⁅ψ⁆ L
⊢ ⁅x.left, x_2.left⁆ + ⁅x_1.left, x_2.left⁆ +
        HAdd.hAdd (α := K) (β := K)
          ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left : K)
          ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x_2.left : K) -
      HAdd.hAdd (α := K) (β := K)
        ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left : K)
        ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x_1.left : K) =
    HSub.hSub (β := K)
        (HAdd.hAdd (β := K) ⁅x.left, x_2.left⁆
          ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left : K))
        ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left : K) +
      HSub.hSub (β := K)
        (HAdd.hAdd (β := K) ⁅x_1.left, x_2.left⁆
          ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x_2.left : K))
        ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x_1.left : K)

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x x_1 x_2 : K ⋊⁅ψ⁆ L
simp :
  ⁅x.left, x_1.left⁆ + ⁅x.left, x_2.left⁆ +
        HAdd.hAdd (α := K) (β := K)
          ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_1.left : K)
          ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left : K) -
      HAdd.hAdd (α := K) (β := K)
        ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x.left : K)
        ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left : K) =
    HSub.hSub (β := K)
        (HAdd.hAdd (β := K) ⁅x.left, x_1.left⁆
          ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_1.left : K))
        ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x.left : K) +
      HSub.hSub (β := K)
        (HAdd.hAdd (β := K) ⁅x.left, x_2.left⁆
          ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left : K))
        ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left : K)
⊢ ⁅x, x_1 + x_2⁆ = ⁅x, x_1⁆ + ⁅x, x_2⁆

Tactic:
simp