awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih :
  ⁅h,
      (HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            n :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (μ - HMul.hMul (α := R) 2 (↑n : R))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
succ :
  HSMul.hSMul (β := M) (-2 + (μ - HMul.hMul (α := R) 2 (↑n : R)))
      (⁅f,
          (HPow.hPow (α := End R M)
                (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
              (a : M) → M)
            m⁆ :
        M) =
    HSMul.hSMul (β := M) (μ - 2 * HAdd.hAdd (α := R) (↑n : R) 1)
      (⁅f,
          (HPow.hPow (α := End R M)
                (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
              (a : M) → M)
            m⁆ :
        M)
⊢ ⁅h,
      (HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            (n + 1) :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (μ - HMul.hMul (α := R) 2 (↑(n + 1) : R))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) (n + 1) :
            (a : M) → M)
          m :
        M)

Tactic:
rw [pow_succ', Module.End.mul_apply, toEnd_apply_apply, Nat.cast_add, Nat.cast_one,
      leibniz_lie h, t.lie_lie_smul_f R, ← neg_smul, ih, lie_smul, smul_lie, ← add_smul]

Premises used: leibniz_lie, neg_smul, IsSl2Triple.lie_lie_smul_f, lie_smul, smul_lie, Nat.cast_add, LieModule.toEnd_apply_apply, add_smul, Module.End.mul_apply, Nat.cast_one, pow_succ'
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih :
  ⁅h,
      (HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            n :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (μ - HMul.hMul (α := R) 2 (↑n : R))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
succ : -2 + (μ - HMul.hMul (α := R) 2 (↑n : R)) = μ - 2 * HAdd.hAdd (α := R) (↑n : R) 1
⊢ HSMul.hSMul (β := M) (-2 + (μ - HMul.hMul (α := R) 2 (↑n : R)))
      (⁅f,
          (HPow.hPow (α := End R M)
                (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
              (a : M) → M)
            m⁆ :
        M) =
    HSMul.hSMul (β := M) (μ - 2 * HAdd.hAdd (α := R) (↑n : R) 1)
      (⁅f,
          (HPow.hPow (α := End R M)
                (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
              (a : M) → M)
            m⁆ :
        M)

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih :
  ⁅h,
      (HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            n :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (μ - HMul.hMul (α := R) 2 (↑n : R))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
⊢ -2 + (μ - HMul.hMul (α := R) 2 (↑n : R)) = μ - 2 * HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
ring
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
zero :
  ⁅h,
      (HPow.hPow (α := End R M) (β := ℕ)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) 0 :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (μ - HMul.hMul (α := R) 2 (↑0 : R))
      ((HPow.hPow (α := End R M) (β := ℕ)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) 0 :
            (a : M) → M)
          m :
        M)
succ :
  ∀ (n : ℕ)
    (ih :
      ⁅h,
          (HPow.hPow (α := End R M)
                (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
              (a : M) → M)
            m⁆ =
        HSMul.hSMul (β := M) (μ - HMul.hMul (α := R) 2 (↑n : R))
          ((HPow.hPow (α := End R M)
                  (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
                (a : M) → M)
              m :
            M)),
    ⁅h,
        (HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) (n + 1) :
            (a : M) → M)
          m⁆ =
      HSMul.hSMul (β := M) (μ - HMul.hMul (α := R) 2 (↑(n + 1) : R))
        ((HPow.hPow (α := End R M)
                (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) (n + 1) :
              (a : M) → M)
            m :
          M)
⊢ ⁅h,
      (HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            n :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (μ - HMul.hMul (α := R) 2 (↑n : R))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)

Tactic:
induction n with
  | zero => simpa using P.lie_h
  | succ n ih =>
    rw [pow_succ', Module.End.mul_apply, toEnd_apply_apply, Nat.cast_add, Nat.cast_one,
      leibniz_lie h, t.lie_lie_smul_f R, ← neg_smul, ih, lie_smul, smul_lie, ← add_smul]
    congr
    ring

Premises used: leibniz_lie, neg_smul, IsSl2Triple.lie_lie_smul_f, lie_smul, smul_lie, Nat.cast_add, LieModule.toEnd_apply_apply, add_smul, IsSl2Triple.HasPrimitiveVectorWith.lie_h, Module.End.mul_apply, Nat.cast_one, pow_succ'
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
⊢ ⁅e,
      (HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            (HAdd.hAdd (α := ℕ) 0 1) :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (HAdd.hAdd (α := R) (↑0 : R) 1 * (μ - (↑0 : R)))
      ((HPow.hPow (α := End R M) (β := ℕ)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) 0 :
            (a : M) → M)
          m :
        M)

Tactic:
simp only [zero_add, pow_one, toEnd_apply_apply, Nat.cast_zero, sub_zero, one_mul,
        pow_zero, Module.End.one_apply, leibniz_lie e, t.lie_e_f, P.lie_e, P.lie_h, lie_zero,
        add_zero]

Premises used: leibniz_lie, sub_zero, zero_add, pow_zero, Module.End.one_apply, IsSl2Triple.HasPrimitiveVectorWith.lie_e, LieModule.toEnd_apply_apply, pow_one, lie_zero, IsSl2Triple.HasPrimitiveVectorWith.lie_h, Nat.cast_zero, add_zero, IsSl2Triple.lie_e_f, one_mul
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih :
  ⁅e,
      (HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            (n + 1) :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (HAdd.hAdd (α := R) (↑n : R) 1 * (μ - (↑n : R)))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
succ :
  HSMul.hSMul (β := M) (μ - 2 * HAdd.hAdd (α := R) (↑n : R) 1 + HAdd.hAdd (α := R) (↑n : R) 1 * (μ - (↑n : R)))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) (n + 1) :
            (a : M) → M)
          m :
        M) =
    HSMul.hSMul (β := M) ((HAdd.hAdd (α := R) (↑n : R) 1 + 1) * (μ - HAdd.hAdd (α := R) (↑n : R) 1))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) (n + 1) :
            (a : M) → M)
          m :
        M)
⊢ ⁅e,
      (HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            (n + 1 + 1) :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (HAdd.hAdd (α := R) (↑(n + 1) : R) 1 * (μ - (↑(n + 1) : R)))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) (n + 1) :
            (a : M) → M)
          m :
        M)

Tactic:
rw [pow_succ', Module.End.mul_apply, toEnd_apply_apply, leibniz_lie e, t.lie_e_f,
      lie_h_pow_toEnd_f P, ih, lie_smul, lie_f_pow_toEnd_f P, ← add_smul,
      Nat.cast_add, Nat.cast_one]

Premises used: leibniz_lie, lie_smul, Nat.cast_add, IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f, LieModule.toEnd_apply_apply, add_smul, IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f, Module.End.mul_apply, Nat.cast_one, IsSl2Triple.lie_e_f, pow_succ'
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih :
  ⁅e,
      (HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            (n + 1) :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (HAdd.hAdd (α := R) (↑n : R) 1 * (μ - (↑n : R)))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
succ :
  μ - 2 * HAdd.hAdd (α := R) (↑n : R) 1 + HAdd.hAdd (α := R) (↑n : R) 1 * (μ - (↑n : R)) =
    (HAdd.hAdd (α := R) (↑n : R) 1 + 1) * (μ - HAdd.hAdd (α := R) (↑n : R) 1)
⊢ HSMul.hSMul (β := M) (μ - 2 * HAdd.hAdd (α := R) (↑n : R) 1 + HAdd.hAdd (α := R) (↑n : R) 1 * (μ - (↑n : R)))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) (n + 1) :
            (a : M) → M)
          m :
        M) =
    HSMul.hSMul (β := M) ((HAdd.hAdd (α := R) (↑n : R) 1 + 1) * (μ - HAdd.hAdd (α := R) (↑n : R) 1))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) (n + 1) :
            (a : M) → M)
          m :
        M)

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih :
  ⁅e,
      (HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            (n + 1) :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (HAdd.hAdd (α := R) (↑n : R) 1 * (μ - (↑n : R)))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
⊢ μ - 2 * HAdd.hAdd (α := R) (↑n : R) 1 + HAdd.hAdd (α := R) (↑n : R) 1 * (μ - (↑n : R)) =
    (HAdd.hAdd (α := R) (↑n : R) 1 + 1) * (μ - HAdd.hAdd (α := R) (↑n : R) 1)

Tactic:
ring
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
zero :
  ⁅e,
      (HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            (HAdd.hAdd (α := ℕ) 0 1) :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (HAdd.hAdd (α := R) (↑0 : R) 1 * (μ - (↑0 : R)))
      ((HPow.hPow (α := End R M) (β := ℕ)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) 0 :
            (a : M) → M)
          m :
        M)
succ :
  ∀ (n : ℕ)
    (ih :
      ⁅e,
          (HPow.hPow (α := End R M)
                (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) (n + 1) :
              (a : M) → M)
            m⁆ =
        HSMul.hSMul (β := M) (HAdd.hAdd (α := R) (↑n : R) 1 * (μ - (↑n : R)))
          ((HPow.hPow (α := End R M)
                  (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
                (a : M) → M)
              m :
            M)),
    ⁅e,
        (HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) (n + 1 + 1) :
            (a : M) → M)
          m⁆ =
      HSMul.hSMul (β := M) (HAdd.hAdd (α := R) (↑(n + 1) : R) 1 * (μ - (↑(n + 1) : R)))
        ((HPow.hPow (α := End R M)
                (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) (n + 1) :
              (a : M) → M)
            m :
          M)
⊢ ⁅e,
      (HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            (n + 1) :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (HAdd.hAdd (α := R) (↑n : R) 1 * (μ - (↑n : R)))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)

Tactic:
induction n with
  | zero =>
      simp only [zero_add, pow_one, toEnd_apply_apply, Nat.cast_zero, sub_zero, one_mul,
        pow_zero, Module.End.one_apply, leibniz_lie e, t.lie_e_f, P.lie_e, P.lie_h, lie_zero,
        add_zero]
  | succ n ih =>
    rw [pow_succ', Module.End.mul_apply, toEnd_apply_apply, leibniz_lie e, t.lie_e_f,
      lie_h_pow_toEnd_f P, ih, lie_smul, lie_f_pow_toEnd_f P, ← add_smul,
      Nat.cast_add, Nat.cast_one]
    congr
    ring

Premises used: leibniz_lie, sub_zero, lie_smul, zero_add, pow_zero, Nat.cast_add, Module.End.one_apply, IsSl2Triple.HasPrimitiveVectorWith.lie_e, IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f, LieModule.toEnd_apply_apply, add_smul, pow_one, IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f, lie_zero, IsSl2Triple.HasPrimitiveVectorWith.lie_h, Nat.cast_zero, Module.End.mul_apply, add_zero, Nat.cast_one, IsSl2Triple.lie_e_f, pow_succ', one_mul
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst_7 : IsNoetherian R M
inst_8 : IsTorsionFree R M
inst_9 : IsDomain R
inst_10 : CharZero R
this :
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
      (0 : M)
obtain :
  ∀ (n : ℕ)
    (hn₁ :
      ¬Eq (α := M)
          ((HPow.hPow (α := End R M)
                  (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
                (a : M) → M)
              m :
            M)
          (0 : M))
    (hn₂ :
      Eq (α := M)
        ((HPow.hPow (α := End R M)
                (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) (n + 1) :
              (a : M) → M)
            m :
          M)
        (0 : M)),
    ∃ (n : ℕ), μ = (↑n : R)
⊢ ∃ (n : ℕ), μ = (↑n : R)

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := Nat.exists_not_and_succ_of_not_zero_of_exists P.ne_zero this

Premises used: Nat.exists_not_and_succ_of_not_zero_of_exists
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst_7 : IsNoetherian R M
inst_8 : IsTorsionFree R M
inst_9 : IsDomain R
inst_10 : CharZero R
this :
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
      (0 : M)
n : ℕ
hn₁ :
  ¬Eq (α := M)
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
      (0 : M)
hn₂ :
  Eq (α := M)
    ((HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            (n + 1) :
          (a : M) → M)
        m :
      M)
    (0 : M)
⊢ ∃ (n : ℕ), μ = (↑n : R)

Tactic:
⟨n, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst_7 : IsNoetherian R M
inst_8 : IsTorsionFree R M
inst_9 : IsDomain R
inst_10 : CharZero R
this :
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
      (0 : M)
n : ℕ
hn₁ :
  ¬Eq (α := M)
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
      (0 : M)
hn₂ :
  Eq (α := M)
    ((HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            (n + 1) :
          (a : M) → M)
        m :
      M)
    (0 : M)
refine : μ = (↑n : R)
⊢ ∃ (n : ℕ), μ = (↑n : R)

Tactic:
refine ⟨n, ?_⟩
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst_7 : IsNoetherian R M
inst_8 : IsTorsionFree R M
inst_9 : IsDomain R
inst_10 : CharZero R
this :
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
      (0 : M)
n : ℕ
hn₁ :
  ¬Eq (α := M)
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
      (0 : M)
hn₂ :
  Eq (α := M)
    ((HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            (n + 1) :
          (a : M) → M)
        m :
      M)
    (0 : M)
⊢ ⁅e,
      (HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            (n + 1) :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (HAdd.hAdd (α := R) (↑n : R) 1 * (μ - (↑n : R)))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)

Tactic:
have := lie_e_pow_succ_toEnd_f P n
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst_7 : IsNoetherian R M
inst_8 : IsTorsionFree R M
inst_9 : IsDomain R
inst_10 : CharZero R
this_1 :
  ∃ (n : ℕ),
    Eq (α := M)
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
      (0 : M)
n : ℕ
hn₁ :
  ¬Eq (α := M)
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
      (0 : M)
hn₂ :
  Eq (α := M)
    ((HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            (n + 1) :
          (a : M) → M)
        m :
      M)
    (0 : M)
this :
  ⁅e,
      (HPow.hPow (α := End R M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M)
            (n + 1) :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (HAdd.hAdd (α := R) (↑n : R) 1 * (μ - (↑n : R)))
      ((HPow.hPow (α := End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) f : End R M) n :
            (a : M) → M)
          m :
        M)
⊢ HAdd.hAdd (α := R) (↑n : R) 1 = 0 ∨ μ = (↑n : R)

Tactic:
rw [hn₂, lie_zero, eq_comm, smul_eq_zero_iff_left hn₁, mul_eq_zero, sub_eq_zero] at this

Premises used: sub_eq_zero, smul_eq_zero_iff_left, eq_comm, mul_eq_zero, lie_zero