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_1 e f : L
m : M
μ : R
t : IsSl2Triple h_1 e f
P : t.HasPrimitiveVectorWith m μ
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : IsNoetherian R M
inst_10 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
h :
  ¬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)
⊢ 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) =
    HSMul.hSMul (β := M) ((↑n : R) - 2 * 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:
simp [hn]
-- 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_1 e f : L
m : M
μ : R
t : IsSl2Triple h_1 e f
P : t.HasPrimitiveVectorWith m μ
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : IsNoetherian R M
inst_10 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
h :
  ¬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)
⊢ 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) =
    0

Tactic:
simp [hn]
-- 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_1 e f : L
m : M
μ : R
t : IsSl2Triple h_1 e f
P : t.HasPrimitiveVectorWith m μ
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : IsNoetherian R M
inst_10 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
h :
  ¬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)
⊢ t.HasPrimitiveVectorWith (M := 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)
    ((↑n : R) - 2 * HAdd.hAdd (α := R) (↑n : R) 1)

Tactic:
have : t.HasPrimitiveVectorWith (ψ (n + 1)) (n - 2 * (n + 1) : R) :=
    { ne_zero := h
      lie_h := (P.lie_h_pow_toEnd_f _).trans (by simp [hn])
      lie_e := (P.lie_e_pow_succ_toEnd_f _).trans (by simp [hn]) }
-- 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_1 e f : L
m : M
μ : R
t : IsSl2Triple h_1 e f
P : t.HasPrimitiveVectorWith m μ
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : IsNoetherian R M
inst_10 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
h :
  ¬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 :
  t.HasPrimitiveVectorWith (M := 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)
    ((↑n : R) - 2 * HAdd.hAdd (α := R) (↑n : R) 1)
obtain : ∀ (m : ℕ) (hm : (↑n : R) - 2 * HAdd.hAdd (α := R) (↑n : R) 1 = (↑m : R)), False
⊢ False

Tactic:
obtain ⟨m, hm⟩ := this.exists_nat

Premises used: IsSl2Triple.HasPrimitiveVectorWith.exists_nat
-- 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_1 e f : L
m_1 : M
μ : R
t : IsSl2Triple h_1 e f
P : t.HasPrimitiveVectorWith m_1 μ
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : IsNoetherian R M
inst_10 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
h :
  ¬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_1 :
        M)
      (0 : M)
this :
  t.HasPrimitiveVectorWith (M := 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_1 :
      M)
    ((↑n : R) - 2 * HAdd.hAdd (α := R) (↑n : R) 1)
m : ℕ
hm : (↑n : R) - 2 * HAdd.hAdd (α := R) (↑n : R) 1 = (↑m : R)
⊢ (↑n : ℤ) < (↑m : ℤ) + 2 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1

Tactic:
lia
-- 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_1 e f : L
m_1 : M
μ : R
t : IsSl2Triple h_1 e f
P : t.HasPrimitiveVectorWith m_1 μ
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : IsNoetherian R M
inst_10 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
h :
  ¬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_1 :
        M)
      (0 : M)
this :
  t.HasPrimitiveVectorWith (M := 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_1 :
      M)
    ((↑n : R) - 2 * HAdd.hAdd (α := R) (↑n : R) 1)
m : ℕ
hm : (↑n : R) - 2 * HAdd.hAdd (α := R) (↑n : R) 1 = (↑m : R)
⊢ (↑n : ℤ) < (↑m : ℤ) + 2 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1

Tactic:
have : (n : ℤ) < m + 2 * (n + 1) := by lia
-- 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_1 e f : L
m_1 : M
μ : R
t : IsSl2Triple h_1 e f
P : t.HasPrimitiveVectorWith m_1 μ
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : IsNoetherian R M
inst_10 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
h :
  ¬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_1 :
        M)
      (0 : M)
this_1 :
  t.HasPrimitiveVectorWith (M := 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_1 :
      M)
    ((↑n : R) - 2 * HAdd.hAdd (α := R) (↑n : R) 1)
m : ℕ
hm : (↑n : R) - 2 * HAdd.hAdd (α := R) (↑n : R) 1 = (↑m : R)
this : (↑n : ℤ) < (↑m : ℤ) + 2 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
⊢ Eq.{u_1 + 1} (α := R) (↑(↑n : ℤ) : R) (↑((↑m : ℤ) + 2 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R)

Tactic:
simpa [sub_eq_iff_eq_add] using hm

Premises used: sub_eq_iff_eq_add
-- 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_1 e f : L
m_1 : M
μ : R
t : IsSl2Triple h_1 e f
P : t.HasPrimitiveVectorWith m_1 μ
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : IsNoetherian R M
inst_10 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
h :
  ¬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_1 :
        M)
      (0 : M)
this_1 :
  t.HasPrimitiveVectorWith (M := 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_1 :
      M)
    ((↑n : R) - 2 * HAdd.hAdd (α := R) (↑n : R) 1)
m : ℕ
hm : (↑n : R) - 2 * HAdd.hAdd (α := R) (↑n : R) 1 = (↑m : R)
this : (↑n : ℤ) < (↑m : ℤ) + 2 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
⊢ False

Tactic:
exact this.ne (Int.cast_injective (α := R) <| by simpa [sub_eq_iff_eq_add] using hm)

Premises used: Int.cast_injective, LT.lt.ne
-- 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
e : L
m : M
n : ℕ
⊢ Eq (α := 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) e : End R M) n :
            (a : M) → M)
          m⁆ :
      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) e : End R M)
            (n + 1) :
          (a : M) → M)
        m :
      M)

Tactic:
simp [pow_succ']

Premises used: 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
hm : ⁅h, 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) e : 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) e : End R M) 0 :
            (a : M) → M)
          m :
        M)

Tactic:
simpa using hm
-- 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
hm : ⁅h, m⁆ = μ • 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) e : 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) e : End R M) n :
            (a : M) → M)
          m :
        M)
succ :
  HSMul.hSMul (β := M) (2 + (μ + HMul.hMul (α := R) 2 (↑n : R)))
      (⁅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) e : End R M) n :
              (a : M) → M)
            m⁆ :
        M) =
    HSMul.hSMul (β := M) (μ + 2 * HAdd.hAdd (α := R) (↑n : R) 1)
      (⁅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) e : 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) e : 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) e : 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, IsSl2Triple.lie_h_e_smul R t, smul_lie, ih, lie_smul, ← add_smul]

Premises used: leibniz_lie, lie_smul, IsSl2Triple.lie_h_e_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
hm : ⁅h, m⁆ = μ • 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) e : 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) e : 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)))
      (⁅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) e : End R M) n :
              (a : M) → M)
            m⁆ :
        M) =
    HSMul.hSMul (β := M) (μ + 2 * HAdd.hAdd (α := R) (↑n : R) 1)
      (⁅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) e : End R M) n :
              (a : M) → M)
            m⁆ :
        M)

Tactic:
congr 1
-- 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
hm : ⁅h, m⁆ = μ • 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) e : 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) e : 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
hm : ⁅h, m⁆ = μ • 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) e : 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) e : 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) e : 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) e : 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) e : 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) e : 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) e : 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) e : End R M) n :
            (a : M) → M)
          m :
        M)

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

Premises used: leibniz_lie, lie_smul, IsSl2Triple.lie_h_e_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
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Nontrivial M
inst_10 : IsTorsionFree R M
inst_11 : Module.Finite R M
inst_12 : IsTriangularizable R L M
t : IsSl2Triple h e f
obtain :
  ∀ (μ₀ : R)
    (hμ₀ :
      End.HasEigenvalue.{u_1, u_3} (M := M)
        (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) h) μ₀),
    ∃ (μ : R) (m : M), m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ
⊢ ∃ (μ : R) (m : M), m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ

Tactic:
obtain ⟨μ₀, hμ₀⟩ := IsTriangularizable.exists_hasEigenvalue R L M h

Premises used: LieModule.IsTriangularizable.exists_hasEigenvalue
-- 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
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Nontrivial M
inst_10 : IsTorsionFree R M
inst_11 : Module.Finite R M
inst_12 : IsTriangularizable R L M
t : IsSl2Triple h e f
μ₀ : R
hμ₀ :
  End.HasEigenvalue.{u_1, u_3} (M := M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) h)
    μ₀
obtain :
  ∀ (m₀ : M)
    (hm₀ : End.HasEigenvector (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) h) μ₀ m₀),
    ∃ (μ : R) (m : M), m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ
⊢ ∃ (μ : R) (m : M), m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ

Tactic:
obtain ⟨m₀, hm₀⟩ := hμ₀.exists_hasEigenvector

Premises used: Module.End.HasEigenvalue.exists_hasEigenvector
-- 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
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Nontrivial M
inst_10 : IsTorsionFree R M
inst_11 : Module.Finite R M
inst_12 : IsTriangularizable R L M
t : IsSl2Triple h e f
μ₀ : R
hμ₀ :
  End.HasEigenvalue.{u_1, u_3} (M := M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) h)
    μ₀
m₀ : M
hm₀ : End.HasEigenvector (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) h) μ₀ m₀
evals : (n : ℕ) → R := fun (n : ℕ) ↦ μ₀ + HMul.hMul (α := R) 2 (↑n : R)
e_vecs : (n : ℕ) → M :=
  fun (n : ℕ) ↦
    (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) e : End R M)
          n :
        (a : M) → M)
      m₀
by_contra! : ∀ (contra : ∀ (k : ℕ), e_vecs k ≠ 0), False
⊢ ∃ (k : ℕ), e_vecs k = 0

Tactic:
by_contra! contra
-- 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
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Nontrivial M
inst_10 : IsTorsionFree R M
inst_11 : Module.Finite R M
inst_12 : IsTriangularizable R L M
t : IsSl2Triple h e f
μ₀ : R
hμ₀ :
  End.HasEigenvalue.{u_1, u_3} (M := M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) h)
    μ₀
m₀ : M
hm₀ : End.HasEigenvector (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) h) μ₀ m₀
evals : (n : ℕ) → R := fun (n : ℕ) ↦ μ₀ + HMul.hMul (α := R) 2 (↑n : R)
e_vecs : (n : ℕ) → M :=
  fun (n : ℕ) ↦
    (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) e : End R M)
          n :
        (a : M) → M)
      m₀
contra : ∀ (k : ℕ), e_vecs k ≠ 0
a b : ℕ
hab : evals a = evals b
⊢ a = b

Tactic:
simpa [evals, add_right_inj, mul_eq_mul_left_iff, Nat.cast_inj] using hab

Premises used: mul_eq_mul_left_iff, Nat.cast_inj, add_right_inj
-- 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
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Nontrivial M
inst_10 : IsTorsionFree R M
inst_11 : Module.Finite R M
inst_12 : IsTriangularizable R L M
t : IsSl2Triple h e f
μ₀ : R
hμ₀ :
  End.HasEigenvalue.{u_1, u_3} (M := M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) h)
    μ₀
m₀ : M
hm₀ : End.HasEigenvector (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) h) μ₀ m₀
evals : (n : ℕ) → R := fun (n : ℕ) ↦ μ₀ + HMul.hMul (α := R) 2 (↑n : R)
e_vecs : (n : ℕ) → M :=
  fun (n : ℕ) ↦
    (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) e : End R M)
          n :
        (a : M) → M)
      m₀
contra : ∀ (k : ℕ), e_vecs k ≠ 0
⊢ Function.Injective evals

Tactic:
have h_inj : Function.Injective evals := fun a b hab ↦ by
      simpa [evals, add_right_inj, mul_eq_mul_left_iff, Nat.cast_inj] using hab
-- 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
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Nontrivial M
inst_10 : IsTorsionFree R M
inst_11 : Module.Finite R M
inst_12 : IsTriangularizable R L M
t : IsSl2Triple h e f
μ₀ : R
hμ₀ :
  End.HasEigenvalue.{u_1, u_3} (M := M) (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) h)
    μ₀
m₀ : M
hm₀ : End.HasEigenvector (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) h) μ₀ m₀
evals : (n : ℕ) → R := fun (n : ℕ) ↦ μ₀ + HMul.hMul (α := R) 2 (↑n : R)
e_vecs : (n : ℕ) → M :=
  fun (n : ℕ) ↦
    (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) e : End R M)
          n :
        (a : M) → M)
      m₀
contra : ∀ (k : ℕ), e_vecs k ≠ 0
h_inj : Function.Injective evals
μ : (↑(range evals) : Type u_1)
set :
  let n := Exists.choose (p := fun (y : ℕ) ↦ evals y = (↑μ : R)) ⋯;
  End.HasEigenvector (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) h) (↑μ : R) (e_vecs n)
⊢ End.HasEigenvector (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) h) (↑μ : R)
    (e_vecs (Exists.choose (p := fun (y : ℕ) ↦ evals y = (↑μ : R)) ⋯))

Tactic:
set n := μ.property.choose

Premises used: Exists.choose, Subtype.property