awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
h :
  ∀ (x y : L),
    Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) y →
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
this : IsSolvable.{u_2} ↥⊤
rwa rwa₁ rwa₂ rwa₃ : IsSolvable.{u_2} ↥⊤
⊢ IsSolvable L

Tactic:
rwa [← solvable_iff_equiv_solvable LieSubalgebra.topEquiv (R := R)]

Premises used: LieSubalgebra.topEquiv, LieAlgebra.solvable_iff_equiv_solvable
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
h :
  ∀ (x y : L),
    Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) y →
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
suffices : IsSolvable.{u_2} ↥⊤
⊢ IsSolvable L

Tactic:
suffices IsSolvable (⊤ : LieIdeal R L) by
    rwa [← solvable_iff_equiv_solvable LieSubalgebra.topEquiv (R := R)]
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
h :
  ∀ (x y : L),
    Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) y →
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
h₁ :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal R L) ⊤ x →
      ∀ (y : L),
        Membership.mem (γ := LieIdeal R L) (Bracket.bracket (L := LieIdeal R L) ⊤ ⊤) y →
          Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
⊢ IsSolvable.{u_2} ↥⊤

Tactic:
apply LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zero

Premises used: LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zero
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
h :
  ∀ (x y : L),
    Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) y →
      Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
⊢ ∀ (x : L),
    Membership.mem (γ := LieIdeal R L) ⊤ x →
      ∀ (y : L),
        Membership.mem (γ := LieIdeal R L) (Bracket.bracket (L := LieIdeal R L) ⊤ ⊤) y →
          Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)

Tactic:
aesop
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
rw : IsSolvable.{u_2} ↥(LieIdeal.killingCompl R L ⊤)
⊢ LE.le (α := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) (radical R L)

Tactic:
rw [← LieIdeal.solvable_iff_le_radical]

Premises used: LieAlgebra.LieIdeal.solvable_iff_le_radical
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
⊢ IsSolvable.{u_2} ↥(LieIdeal.killingCompl R L ⊤)

Tactic:
LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zero _ ?_

Premises used: LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zero
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
refine :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) x →
      ∀ (y : L),
        Membership.mem (γ := LieIdeal R L)
            (Bracket.bracket (L := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) (LieIdeal.killingCompl R L ⊤)) y →
          Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
⊢ IsSolvable.{u_2} ↥(LieIdeal.killingCompl R L ⊤)

Tactic:
refine LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zero _ ?_

Premises used: LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zero
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) x
y : L
_ :
  Membership.mem (γ := LieIdeal R L)
      (Bracket.bracket (L := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) (LieIdeal.killingCompl R L ⊤)) y →
    Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
⊢ Membership.mem (γ := LieIdeal R L)
      (Bracket.bracket (L := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) (LieIdeal.killingCompl R L ⊤)) y →
    Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)

Tactic:
_
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) x
y : L
h :
  Membership.mem (γ := LieIdeal R L)
    (Bracket.bracket (L := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) (LieIdeal.killingCompl R L ⊤)) y
rw :
  Eq.{u_1 + 1} (α := R) ((((LieModule.traceForm R L L : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) x : R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)

Tactic:
rw [LieModule.traceForm_comm]

Premises used: LieModule.traceForm_comm
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) x
y : L
h :
  Membership.mem (γ := LieIdeal R L)
    (Bracket.bracket (L := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) (LieIdeal.killingCompl R L ⊤)) y
⊢ Eq.{u_1 + 1} (α := R) ((((LieModule.traceForm R L L : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) x : R)
    (0 : R)

Tactic:
(LieIdeal.mem_killingCompl R L ⊤).mp hx y (LieSubmodule.mem_top y)

Premises used: LieIdeal.mem_killingCompl, Iff.mp, LieSubmodule.mem_top, Top.top
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) x
y : L
h :
  Membership.mem (γ := LieIdeal R L)
    (Bracket.bracket (L := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) (LieIdeal.killingCompl R L ⊤)) y
⊢ Eq.{u_1 + 1} (α := R) ((((LieModule.traceForm R L L : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) x : R)
    (0 : R)

Tactic:
exact (LieIdeal.mem_killingCompl R L ⊤).mp hx y (LieSubmodule.mem_top y)

Premises used: LieIdeal.mem_killingCompl, Iff.mp, LieSubmodule.mem_top, Top.top
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
inst_7 : HasTrivialRadical R L
⊢ Eq (α := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) ⊥

Tactic:
simpa using killingCompl_top_le_radical R L

Premises used: LieAlgebra.killingCompl_top_le_radical
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
inst_7 : IsPrincipalIdealRing R
⊢ HasTrivialRadical R L ↔ IsKilling R L

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.Algebra.Lie.CartanCriterion
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
A : Type u_4
inst_7 : LieRing A
inst_8 : Module.Finite ℤ A
inst_9 : Module.Free ℤ A
⊢ HasTrivialRadical ℤ A ↔ IsKilling ℤ A

Tactic:
hasTrivialRadical_iff_isKilling ℤ A

Premises used: LieAlgebra.hasTrivialRadical_iff_isKilling, Int
-- Module: Mathlib.Algebra.Lie.CartanExists
Goal:
R : Type u_2
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 : Module.Finite R L
inst_8 : Free R L
inst_9 : Module.Finite R M
inst_10 : Free R M
x y : L
⊢ Monic (R := R[X]) (lieCharpoly R M x y)

Tactic:
(polyCharpoly_monic _ _).map _

Premises used: _private.0.LieAlgebra.engel_isBot_of_isMin.lieCharpoly, LinearMap.polyCharpoly_monic, Polynomial.Monic.map
-- Module: Mathlib.Algebra.Lie.CartanExists
Goal:
R : Type u_2
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 : Module.Finite R L
inst_8 : Free R L
inst_9 : Module.Finite R M
inst_10 : Free R M
x y : L
inst_11 : Nontrivial R
rw :
  natDegree
      (Polynomial.map
        (↑(MvPolynomial.aeval fun (i : ChooseBasisIndex R L) ↦
              HAdd.hAdd (β := R[X])
                (HMul.hMul (α := R[X]) (β := R[X])
                  ((C : (a : R) → R[X])
                      ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) y :
                            Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                          (a : ChooseBasisIndex R L) → R)
                        i) :
                    R[X])
                  X)
                ((C : (a : R) → R[X])
                    ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) x :
                          Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                        (a : ChooseBasisIndex R L) → R)
                      i) :
                  R[X])) :
          MvPolynomial (ChooseBasisIndex R L) R →+* R[X])
        (polyCharpoly (↑φ : L →ₗ[R] End R M) (chooseBasis R L))) =
    finrank R M
rw₁ :
  natDegree (R := MvPolynomial.{u_3, u_2} (ChooseBasisIndex R L) R)
      (polyCharpoly (↑φ : L →ₗ[R] End R M) (chooseBasis R L)) =
    finrank R M
rw₂ rw₃ : finrank R M = finrank R M
⊢ natDegree (R := R[X]) (lieCharpoly R M x y) = finrank R M

Tactic:
rw [lieCharpoly, (polyCharpoly_monic _ _).natDegree_map, polyCharpoly_natDegree]

Premises used: _private.0.LieAlgebra.engel_isBot_of_isMin.lieCharpoly, Polynomial.Monic.natDegree_map, LinearMap.polyCharpoly_monic, LinearMap.polyCharpoly_natDegree
-- Module: Mathlib.Algebra.Lie.CartanExists
Goal:
R : Type u_2
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 : Module.Finite R L
inst_8 : Free R L
inst_9 : Module.Finite R M
inst_10 : Free R M
x y : L
r : R
rw :
  Polynomial.map
      (RingHom.comp (evalRingHom r)
        (↑(MvPolynomial.aeval fun (i : ChooseBasisIndex R L) ↦
              HAdd.hAdd (β := R[X])
                (HMul.hMul (α := R[X]) (β := R[X])
                  ((C : (a : R) → R[X])
                      ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) y :
                            Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                          (a : ChooseBasisIndex R L) → R)
                        i) :
                    R[X])
                  X)
                ((C : (a : R) → R[X])
                    ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) x :
                          Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                        (a : ChooseBasisIndex R L) → R)
                      i) :
                  R[X])) :
          MvPolynomial (ChooseBasisIndex R L) R →+* R[X]))
      (polyCharpoly (↑φ : L →ₗ[R] End R M) (chooseBasis R L)) =
    charpoly.{u_2, u_4} (M := M) (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y + x))
⊢ Eq (α := R[X]) (Polynomial.map (evalRingHom r) (lieCharpoly R M x y))
    (charpoly.{u_2, u_4} (M := M) (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y + x)))

Tactic:
rw [lieCharpoly, map_map]

Premises used: _private.0.LieAlgebra.engel_isBot_of_isMin.lieCharpoly, Polynomial.map_map
-- Module: Mathlib.Algebra.Lie.CartanExists
Goal:
R : Type u_2
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 : Module.Finite R L
inst_8 : Free R L
inst_9 : Module.Finite R M
inst_10 : Free R M
x y : L
r : R
set :
  let b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L;
  Polynomial.map
      (RingHom.comp (evalRingHom r)
        (↑(MvPolynomial.aeval fun (i : ChooseBasisIndex R L) ↦
              HAdd.hAdd (β := R[X])
                (HMul.hMul (α := R[X]) (β := R[X])
                  ((C : (a : R) → R[X])
                      ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) y :
                            Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                          (a : ChooseBasisIndex R L) → R)
                        i) :
                    R[X])
                  X)
                ((C : (a : R) → R[X])
                    ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) x : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                        (a : ChooseBasisIndex R L) → R)
                      i) :
                  R[X])) :
          MvPolynomial (ChooseBasisIndex R L) R →+* R[X]))
      (polyCharpoly (↑φ : L →ₗ[R] End R M) b) =
    charpoly.{u_2, u_4} (M := M) (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y + x))
⊢ Polynomial.map
      (RingHom.comp (evalRingHom r)
        (↑(MvPolynomial.aeval fun (i : ChooseBasisIndex R L) ↦
              HAdd.hAdd (β := R[X])
                (HMul.hMul (α := R[X]) (β := R[X])
                  ((C : (a : R) → R[X])
                      ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) y :
                            Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                          (a : ChooseBasisIndex R L) → R)
                        i) :
                    R[X])
                  X)
                ((C : (a : R) → R[X])
                    ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) x :
                          Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                        (a : ChooseBasisIndex R L) → R)
                      i) :
                  R[X])) :
          MvPolynomial (ChooseBasisIndex R L) R →+* R[X]))
      (polyCharpoly (↑φ : L →ₗ[R] End R M) (chooseBasis R L)) =
    charpoly.{u_2, u_4} (M := M) (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y + x))

Tactic:
set b := chooseBasis R L

Premises used: Module.Free.chooseBasis
-- Module: Mathlib.Algebra.Lie.CartanExists
Goal:
R : Type u_2
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 : Module.Finite R L
inst_8 : Free R L
inst_9 : Module.Finite R M
inst_10 : Free R M
x y : L
r : R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
h :
  ∀ (i : ChooseBasisIndex R L),
    HAdd.hAdd (β := R)
        (HMul.hMul (α := R)
          ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) y : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                (a : ChooseBasisIndex R L) → R)
              i :
            R)
          r)
        ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) x : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
              (a : ChooseBasisIndex R L) → R)
            i :
          R) =
      (((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) (r • y + x) : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
          (a : ChooseBasisIndex R L) → R)
        i
⊢ Eq (α := (i : ChooseBasisIndex R L) → R)
    (fun (i : ChooseBasisIndex R L) ↦
      HAdd.hAdd (β := R)
        (HMul.hMul (α := R)
          ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) y : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                (a : ChooseBasisIndex R L) → R)
              i :
            R)
          r)
        ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) x : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
              (a : ChooseBasisIndex R L) → R)
            i :
          R))
    (⇑((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) (r • y + x) : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
      (a : ChooseBasisIndex R L) → R)

Tactic:
ext i
-- Module: Mathlib.Algebra.Lie.CartanExists
Goal:
R : Type u_2
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 : Module.Finite R L
inst_8 : Free R L
inst_9 : Module.Finite R M
inst_10 : Free R M
x y : L
r : R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
i : ChooseBasisIndex R L
⊢ HAdd.hAdd (β := R)
      (HMul.hMul (α := R)
        ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) y : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
              (a : ChooseBasisIndex R L) → R)
            i :
          R)
        r)
      ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) x : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
            (a : ChooseBasisIndex R L) → R)
          i :
        R) =
    (((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) (r • y + x) : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
        (a : ChooseBasisIndex R L) → R)
      i

Tactic:
simp [mul_comm r]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Lie.CartanExists
Goal:
R : Type u_2
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 : Module.Finite R L
inst_8 : Free R L
inst_9 : Module.Finite R M
inst_10 : Free R M
x y : L
r : R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
⊢ Eq (α := (i : ChooseBasisIndex R L) → R)
    (fun (i : ChooseBasisIndex R L) ↦
      HAdd.hAdd (β := R)
        (HMul.hMul (α := R)
          ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) y : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                (a : ChooseBasisIndex R L) → R)
              i :
            R)
          r)
        ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) x : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
              (a : ChooseBasisIndex R L) → R)
            i :
          R))
    (⇑((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) (r • y + x) : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
      (a : ChooseBasisIndex R L) → R)

Tactic:
have aux : (fun i ↦ (b.repr y) i * r + (b.repr x) i) = b.repr (r • y + x) := by
    ext i; simp [mul_comm r]
-- Module: Mathlib.Algebra.Lie.CartanExists
Goal:
R : Type u_2
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 : Module.Finite R L
inst_8 : Free R L
inst_9 : Module.Finite R M
inst_10 : Free R M
x y : L
inst_11 : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
rw :
  natDegree.{u_2} (R := R)
      (((↑(MvPolynomial.aeval fun (i : ChooseBasisIndex R L) ↦
                HAdd.hAdd (β := R[X])
                  (HMul.hMul (α := R[X]) (β := R[X])
                    ((C : (a : R) → R[X])
                        ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) y :
                              Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                            (a : ChooseBasisIndex R L) → R)
                          i) :
                      R[X])
                    X)
                  ((C : (a : R) → R[X])
                      ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) x :
                            Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                          (a : ChooseBasisIndex R L) → R)
                        i) :
                    R[X])) :
            MvPolynomial (ChooseBasisIndex R L) R →+* R[X]) :
          (a : MvPolynomial (ChooseBasisIndex R L) R) → R[X])
        (coeff (polyCharpoly (↑φ : L →ₗ[R] End R M) (chooseBasis R L)) i)) ≤
    j * 1
⊢ natDegree (coeff (lieCharpoly R M x y) i) ≤ j

Tactic:
rw [← mul_one j, lieCharpoly, coeff_map]

Premises used: Polynomial.coeff_map, _private.0.LieAlgebra.engel_isBot_of_isMin.lieCharpoly, mul_one
-- Module: Mathlib.Algebra.Lie.CartanExists
Goal:
R : Type u_2
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 : Module.Finite R L
inst_8 : Free R L
inst_9 : Module.Finite R M
inst_10 : Free R M
x y : L
inst_11 : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
hF :
  MvPolynomial.totalDegree (σ := ChooseBasisIndex R L)
      (coeff (polyCharpoly (↑φ : L →ₗ[R] End R M) (chooseBasis R L)) i) ≤
    j
hf :
  ∀ (i : ChooseBasisIndex R L),
    (HAdd.hAdd (β := R[X])
          (HMul.hMul (α := R[X]) (β := R[X])
            ((C : (a : R) → R[X])
                ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) y :
                      Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                    (a : ChooseBasisIndex R L) → R)
                  i) :
              R[X])
            X)
          ((C : (a : R) → R[X])
              ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) x :
                    Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                  (a : ChooseBasisIndex R L) → R)
                i) :
            R[X])).natDegree ≤
      1
⊢ natDegree.{u_2} (R := R)
      (((↑(MvPolynomial.aeval fun (i : ChooseBasisIndex R L) ↦
                HAdd.hAdd (β := R[X])
                  (HMul.hMul (α := R[X]) (β := R[X])
                    ((C : (a : R) → R[X])
                        ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) y :
                              Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                            (a : ChooseBasisIndex R L) → R)
                          i) :
                      R[X])
                    X)
                  ((C : (a : R) → R[X])
                      ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) x :
                            Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                          (a : ChooseBasisIndex R L) → R)
                        i) :
                    R[X])) :
            MvPolynomial (ChooseBasisIndex R L) R →+* R[X]) :
          (a : MvPolynomial (ChooseBasisIndex R L) R) → R[X])
        (coeff (polyCharpoly (↑φ : L →ₗ[R] End R M) (chooseBasis R L)) i)) ≤
    j * 1

Tactic:
apply MvPolynomial.aeval_natDegree_le

Premises used: MvPolynomial.aeval_natDegree_le