-- Mathlib/Algebra/Lie/Sl2.lean
/-- The eigenvalue of a primitive vector must be a natural number if the representation is
finite-dimensional. -/
lemma exists_nat [IsNoetherian R M] [NoZeroSMulDivisors R M] [IsDomain R] [CharZero R] :
    ∃ n : ℕ, μ = n

Proof state:
case intro.intro
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsNoetherian R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : ∃ n, ((toEnd R L M) f ^ n) m = 0
n : ℕ
hn₁ : ¬((toEnd R L M) f ^ n) m = 0
hn₂ : ((toEnd R L M) f ^ (n + 1)) m = 0
⊢ μ = ↑n

Tactic:
have := lie_e_pow_succ_toEnd_f P n

Result:
case intro.intro
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsNoetherian R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
this✝ : ∃ n, ((toEnd R L M) f ^ n) m = 0
n : ℕ
hn₁ : ¬((toEnd R L M) f ^ n) m = 0
hn₂ : ((toEnd R L M) f ^ (n + 1)) m = 0
this : ⁅e, ((toEnd R L M) f ^ (n + 1)) m⁆ = ((↑n + 1) * (μ - ↑n)) • ((toEnd R L M) f ^ n) m
⊢ μ = ↑n

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsNoetherian R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
⊢ Infinite ℕ

Tactic:
infer_instance

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsNoetherian R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
hs : (range fun n => μ - 2 * ↑n).Infinite
contra : ∀ (n : ℕ), ((toEnd R L M) f ^ n) m ≠ 0
x✝ : ↑{x | ∃ n, μ - 2 * ↑n = x}
r : R
hr : r ∈ {x | ∃ n, μ - 2 * ↑n = x}
⊢ ((toEnd R L M) h).HasEigenvector (↑⟨r, hr⟩)
    ((fun x =>
        match x with
        | ⟨s, hs⟩ => ((toEnd R L M) f ^ Classical.choose hs) m)
      ⟨r, hr⟩)

Tactic:
simp [lie_h_pow_toEnd_f P, Classical.choose_spec hr, contra,
Module.End.hasEigenvector_iff, Module.End.mem_eigenspace_iff]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsNoetherian R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
hs : (range fun n => μ - 2 * ↑n).Infinite
contra : ∀ (n : ℕ), ((toEnd R L M) f ^ n) m ≠ 0
⊢ False

Tactic:
exact hs ((toEnd R L M h).eigenvectors_linearIndependent
  {μ - 2 * n | n : ℕ}
  (fun ⟨s, hs⟩ ↦ ψ Classical.choose hs)
  (fun ⟨r, hr⟩ ↦ by simp [lie_h_pow_toEnd_f P, Classical.choose_spec hr, contra,
    Module.End.hasEigenvector_iff, Module.End.mem_eigenspace_iff])).finite

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
h e f : L
m✝ : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m✝ μ
inst✝³ : IsNoetherian R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
n m : ℕ
⊢ μ - 2 * ↑n = μ - 2 * ↑m → n = m

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsNoetherian R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : ∃ n, ((toEnd R L M) f ^ n) m = 0
⊢ ∃ n, μ = ↑n

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

Result:
case intro.intro
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsNoetherian R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
this : ∃ n, ((toEnd R L M) f ^ n) m = 0
n : ℕ
hn₁ : ¬((toEnd R L M) f ^ n) m = 0
hn₂ : ((toEnd R L M) f ^ (n + 1)) m = 0
⊢ ∃ n, μ = ↑n

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsNoetherian R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
⊢ ∃ n, ((toEnd R L M) f ^ n) m = 0

Tactic:
have hs : (range <| fun (n : ℕ) ↦ μ - 2 * n).Infinite := by
  rw [infinite_range_iff (fun n m ↦ by simp)]; infer_instance

Result:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsNoetherian R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
hs : (range fun n => μ - 2 * ↑n).Infinite
⊢ ∃ n, ((toEnd R L M) f ^ n) m = 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsNoetherian R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
⊢ ∃ n, μ = ↑n

Tactic:
suffices ∃ n : ℕ, (ψ n) = 0 by
  obtain ⟨n, hn₁, hn₂⟩ := Nat.exists_not_and_succ_of_not_zero_of_exists P.ne_zero this
  refine ⟨n, ?_⟩
  have := lie_e_pow_succ_toEnd_f P n
  rw [hn₂, lie_zero, eq_comm, smul_eq_zero_iff_left hn₁, mul_eq_zero, sub_eq_zero] at this
  exact this.resolve_left <| Nat.cast_add_one_ne_zero n

Result:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝³ : IsNoetherian R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : IsDomain R
inst✝ : CharZero R
⊢ ∃ n, ((toEnd R L M) f ^ n) m = 0