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
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)
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)

Tactic:
⟨?_, contra n⟩

Premises used: Module.End.HasUnifEigenvector, And.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
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)
n : ℕ := Exists.choose (p := fun (y : ℕ) ↦ evals y = (↑μ : R)) ⋯
refine :
  Membership.mem (γ := Submodule R M)
    ((End.genEigenspace (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) h) (↑μ : R) :
          (a : ℕ∞) → Submodule R M)
        1 :
      Submodule R M)
    (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 n)

Tactic:
refine ⟨?_, contra 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
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)
n : ℕ := Exists.choose (p := fun (y : ℕ) ↦ evals y = (↑μ : R)) ⋯
rw : ⁅h, e_vecs n⁆ = evals (Exists.choose (p := fun (y : ℕ) ↦ evals y = (↑μ : R)) ⋯) • e_vecs n
⊢ Membership.mem (γ := Submodule R M)
    ((End.genEigenspace (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (End R M)) : (a : L) → End R M) h) (↑μ : R) :
          (a : ℕ∞) → Submodule R M)
        1 :
      Submodule R M)
    (e_vecs n)

Tactic:
rw [Module.End.mem_eigenspace_iff, toEnd_apply_apply, ← μ.property.choose_spec]

Premises used: Exists.choose_spec, Module.End.mem_eigenspace_iff, LieModule.toEnd_apply_apply, Subtype.property
-- 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)
n : ℕ := Exists.choose (p := fun (y : ℕ) ↦ evals y = (↑μ : R)) ⋯
⊢ ⁅h, e_vecs n⁆ = evals (Exists.choose (p := fun (y : ℕ) ↦ evals y = (↑μ : R)) ⋯) • e_vecs n

Tactic:
t.lie_h_pow_toEnd_e hm₀.apply_eq_smul n

Premises used: Module.End.HasEigenvector.apply_eq_smul, IsSl2Triple.lie_h_pow_toEnd_e
-- 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)
n : ℕ := Exists.choose (p := fun (y : ℕ) ↦ evals y = (↑μ : R)) ⋯
⊢ ⁅h, e_vecs n⁆ = evals (Exists.choose (p := fun (y : ℕ) ↦ evals y = (↑μ : R)) ⋯) • e_vecs n

Tactic:
exact t.lie_h_pow_toEnd_e hm₀.apply_eq_smul n

Premises used: Module.End.HasEigenvector.apply_eq_smul, IsSl2Triple.lie_h_pow_toEnd_e
-- 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)),
    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:
have aux (μ : range evals) : (toEnd R L M h).HasEigenvector μ (e_vecs μ.property.choose) := by
      set n := μ.property.choose
      refine ⟨?_, contra n⟩
      rw [Module.End.mem_eigenspace_iff, toEnd_apply_apply, ← μ.property.choose_spec]
      exact t.lie_h_pow_toEnd_e hm₀.apply_eq_smul 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
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
aux :
  ∀ (μ : (↑(range evals) : Type u_1)),
    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)) ⋯))
⊢ Finite.{u_1 + 1} (↑(range evals) : Type u_1)

Tactic:
have _i := ((toEnd R L M h).eigenvectors_linearIndependent (range evals) _ aux).finite
-- 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
aux :
  ∀ (μ : (↑(range evals) : Type u_1)),
    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)) ⋯))
_i : Finite.{u_1 + 1} (↑(range evals) : Type u_1)
⊢ False

Tactic:
(Set.infinite_range_of_injective h_inj) (Set.toFinite _)

Premises used: Set.infinite_range_of_injective, Set.toFinite
-- 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
aux :
  ∀ (μ : (↑(range evals) : Type u_1)),
    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)) ⋯))
_i : Finite.{u_1 + 1} (↑(range evals) : Type u_1)
⊢ False

Tactic:
exact (Set.infinite_range_of_injective h_inj) (Set.toFinite _)

Premises used: Set.infinite_range_of_injective, Set.toFinite
-- 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₀
⊢ ∃ (k : ℕ), e_vecs k = 0

Tactic:
have h_exists_zero : ∃ k, e_vecs k = 0 := by
    by_contra! contra
    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
    have aux (μ : range evals) : (toEnd R L M h).HasEigenvector μ (e_vecs μ.property.choose) := by
      set n := μ.property.choose
      refine ⟨?_, contra n⟩
      rw [Module.End.mem_eigenspace_iff, toEnd_apply_apply, ← μ.property.choose_spec]
      exact t.lie_h_pow_toEnd_e hm₀.apply_eq_smul n
    have _i := ((toEnd R L M h).eigenvectors_linearIndependent (range evals) _ aux).finite
    exact (Set.infinite_range_of_injective h_inj) (Set.toFinite _)
-- 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₀
h_exists_zero : ∃ (k : ℕ), e_vecs k = 0
obtain :
  ∀ (n : ℕ) (hn_ne : ¬e_vecs n = 0) (hn_zero : e_vecs (n + 1) = 0),
    ∃ (μ : R) (m : M), m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ
⊢ ∃ (μ : R) (m : M), m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ

Tactic:
obtain ⟨n, hn_ne, hn_zero⟩ := Nat.exists_not_and_succ_of_not_zero_of_exists hm₀.2 h_exists_zero

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
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₀
h_exists_zero : ∃ (k : ℕ), e_vecs k = 0
n : ℕ
hn_ne : ¬e_vecs n = 0
hn_zero : e_vecs (n + 1) = 0
rwa rwa₁ rwa₂ rwa₃ :
  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) e : End R M)
            (n + 1) :
          (a : M) → M)
        m₀ :
      M)
    (0 : M)
⊢ ⁅e, e_vecs n⁆ = 0

Tactic:
rwa [lie_e_pow_toEnd_e n]

Premises used: IsSl2Triple.lie_e_pow_toEnd_e
-- 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₀
h_exists_zero : ∃ (k : ℕ), e_vecs k = 0
n : ℕ
hn_ne : ¬e_vecs n = 0
hn_zero : e_vecs (n + 1) = 0
⊢ ∃ (μ : R) (m : M), m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ

Tactic:
exact ⟨evals n, e_vecs n, hn_ne,
    { ne_zero := hn_ne
      lie_h := t.lie_h_pow_toEnd_e hm₀.apply_eq_smul n
      lie_e := by rwa [lie_e_pow_toEnd_e n] }⟩
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ derivedSeriesOfIdeal R L 0 I = I

Tactic:
rfl

Premises used: Nat.iterate, LieAlgebra.derivedSeriesOfIdeal, rfl
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ derivedSeriesOfIdeal R L (k + 1) I = ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆

Tactic:
Function.iterate_succ_apply' (fun I => ⁅I, I⁆) k I

Premises used: Function.iterate_succ_apply', Set.Mem, Bracket.bracket, setOf, LieAlgebra.derivedSeriesOfIdeal
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
k : ℕ
⊢ Eq (α := LieIdeal R L) (derivedSeries R L k) (derivedSeriesOfIdeal R L k ⊤)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h :
  ∀ (z : L),
    Membership.mem (γ := Submodule R L) (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra R L (derivedSeries R L 1)))
        z ↔
      Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (x_1 : L) (y : L), ⁅x_1, y⁆ = x}) z
⊢ Eq (α := Submodule R L) (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra R L (derivedSeries R L 1)))
    (Submodule.span R {x : L | ∃ (x_1 : L) (y : L), ⁅x_1, y⁆ = x})

Tactic:
ext z
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
z : L
h :
  Membership.mem (γ := Submodule R L)
      (Submodule.span R
        {x : L |
          ∃ (x_1 : L),
            Membership.mem (γ := LieIdeal R L) ⊤ x_1 ∧
              ∃ (n : L), Membership.mem (γ := LieSubmodule R L L) ⊤ n ∧ ⁅x_1, n⁆ = x})
      z ↔
    Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (x_1 : L) (y : L), ⁅x_1, y⁆ = x}) z
⊢ Membership.mem (γ := Submodule R L) (LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra R L (derivedSeries R L 1)))
      z ↔
    Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (x_1 : L) (y : L), ⁅x_1, y⁆ = x}) z

Tactic:
simp only [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero,
    LieIdeal.toLieSubalgebra_toSubmodule, LieSubmodule.lieIdeal_oper_eq_linear_span']

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span', LieIdeal.toLieSubalgebra_toSubmodule, LieAlgebra.derivedSeriesOfIdeal_succ, LieAlgebra.derivedSeriesOfIdeal_zero
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
z : L
⊢ Membership.mem (γ := Submodule R L)
      (Submodule.span R
        {x : L |
          ∃ (x_1 : L),
            Membership.mem (γ := LieIdeal R L) ⊤ x_1 ∧
              ∃ (n : L), Membership.mem (γ := LieSubmodule R L L) ⊤ n ∧ ⁅x_1, n⁆ = x})
      z ↔
    Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (x_1 : L) (y : L), ⁅x_1, y⁆ = x}) z

Tactic:
aesop
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
l : ℕ
zero : D l I = D 0 (D l I)
zero₁ zero₂ : D l I = D l I
⊢ D (0 + l) I = D 0 (D l I)

Tactic:
rw [Nat.zero_add, derivedSeriesOfIdeal_zero]

Premises used: Nat.zero_add, LieAlgebra.derivedSeriesOfIdeal_zero
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
l k : ℕ
ih : D (k + l) I = D k (D l I)
succ : D (k + l).succ I = D (k + 1) (D l I)
succ₁ : ⁅D (k + l) I, D (k + l) I⁆ = D (k + 1) (D l I)
succ₂ : ⁅D (k + l) I, D (k + l) I⁆ = ⁅D k (D l I), D k (D l I)⁆
succ₃ succ₄ : ⁅D k (D l I), D k (D l I)⁆ = ⁅D k (D l I), D k (D l I)⁆
⊢ D (k + 1 + l) I = D (k + 1) (D l I)

Tactic:
rw [Nat.succ_add k l, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ, ih]

Premises used: LieAlgebra.derivedSeriesOfIdeal_succ, Nat.succ_add
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k l : ℕ
zero : D (0 + l) I = D 0 (D l I)
succ : ∀ (k : ℕ) (ih : D (k + l) I = D k (D l I)), D (k + 1 + l) I = D (k + 1) (D l I)
⊢ D (k + l) I = D k (D l I)

Tactic:
induction k with
  | zero => rw [Nat.zero_add, derivedSeriesOfIdeal_zero]
  | succ k ih => rw [Nat.succ_add k l, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ, ih]

Premises used: LieAlgebra.derivedSeriesOfIdeal_succ, Nat.zero_add, Nat.succ_add, LieAlgebra.derivedSeriesOfIdeal_zero
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l ≤ 0
⊢ l = 0

Tactic:
rw [le_zero_iff] at h₂

Premises used: le_zero_iff
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
zero : I ≤ D 0 J
⊢ D 0 I ≤ D l J

Tactic:
rw [h₂, derivedSeriesOfIdeal_zero]

Premises used: LieAlgebra.derivedSeriesOfIdeal_zero
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ I ≤ D 0 J

Tactic:
h₁

Premises used: Set.Mem
-- Module: Mathlib.Algebra.Lie.Solvable
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
l : ℕ
h₂ : l = 0
⊢ I ≤ D 0 J

Tactic:
exact h₁