awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
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 : ℕ
⊢ ⁅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)
have 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)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
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)
⊢ ⁅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)
have 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)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
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) (m : M), m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ
have 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 μ
Tactic: obtain ⟨μ₀, hμ₀⟩ := IsTriangularizable.exists_hasEigenvalue R L M h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
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)
    μ₀
⊢ ∃ (μ : R) (m : M), m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ
have 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 μ
Tactic: obtain ⟨m₀, hm₀⟩ := hμ₀.exists_hasEigenvector
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
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
have by_contra! : ∀ (contra : ∀ (k : ℕ), e_vecs k ≠ 0), False
Tactic: by_contra! contra
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (hypothesis)
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
⊢ False
have h_inj : 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
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)
have 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)
Tactic: refine ⟨?_, contra n⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
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)) ⋯
⊢ 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)
have rw : ⁅h, e_vecs n⁆ = evals (Exists.choose (p := fun (y : ℕ) ↦ evals y = (↑μ : R)) sorry) • e_vecs n
Tactic: rw [Module.End.mem_eigenspace_iff, toEnd_apply_apply, ← μ.property.choose_spec]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (hypothesis)
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
⊢ False
have 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)) sorry))
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
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (hypothesis)
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)) ⋯))
⊢ False
have _i : Finite.{u_1 + 1} (↑(range evals) : Type u_1)
Tactic: have _i := ((toEnd R L M h).eigenvectors_linearIndependent (range evals) _ aux).finite
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (hypothesis)
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₀
⊢ ∃ (μ : R) (m : M), m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ
have h_exists_zero : ∃ (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 _)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
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
⊢ ∃ (μ : R) (m : M), m ≠ 0 ∧ t.HasPrimitiveVectorWith m μ
have obtain : ∀ (n : ℕ) (hn_ne : ¬e_vecs n = 0) (hn_zero : e_vecs (n + 1) = 0),
  ∃ (μ : 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ 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})
have 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
Tactic: ext z
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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) (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
have 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
Tactic: simp only [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero,
    LieIdeal.toLieSubalgebra_toSubmodule, LieSubmodule.lieIdeal_oper_eq_linear_span']
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
l : ℕ
⊢ D (0 + l) I = D 0 (D l I)
have zero : D l I = D 0 (D l I)
Tactic: rw [Nat.zero_add, derivedSeriesOfIdeal_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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)
⊢ D (0 + l) I = D 0 (D l I)
have zero₁ : D l I = D l I
Tactic: rw [Nat.zero_add, derivedSeriesOfIdeal_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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)
⊢ D (k + 1 + l) I = D (k + 1) (D l I)
have succ : D (k + l).succ I = D (k + 1) (D l I)
Tactic: rw [Nat.succ_add k l, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ, ih]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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)
⊢ D (k + 1 + l) I = D (k + 1) (D l I)
have succ₁ : ⁅D (k + l) I, D (k + l) I⁆ = D (k + 1) (D l I)
Tactic: rw [Nat.succ_add k l, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ, ih]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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)
⊢ D (k + 1 + l) I = D (k + 1) (D l I)
have succ₂ : ⁅D (k + l) I, D (k + l) I⁆ = ⁅D k (D l I), D k (D l I)⁆
Tactic: rw [Nat.succ_add k l, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ, ih]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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)⁆
⊢ D (k + 1 + l) I = D (k + 1) (D l I)
have succ₃ : ⁅D k (D l I), D k (D l I)⁆ = ⁅D k (D l I), D k (D l I)⁆
Tactic: rw [Nat.succ_add k l, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ, ih]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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 : ℕ
⊢ D (k + l) I = D k (D l I)
have zero : D (0 + l) I = D 0 (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]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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)
⊢ D (k + l) I = D k (D l I)
have succ : ∀ (k : ℕ) (ih : D (k + l) I = D k (D l I)), D (k + 1 + l) I = D (k + 1) (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]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (hypothesis)
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
⊢ D 0 I ≤ D l J
have h₃ : l = 0
Tactic: rw [le_zero_iff] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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
⊢ D 0 I ≤ D l J
have zero : I ≤ D 0 J
Tactic: rw [h₂, derivedSeriesOfIdeal_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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
k : ℕ
ih : ∀ {l : ℕ} (h₂ : l ≤ k), D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
⊢ l = k.succ ∨ l ≤ k
have rwa : ∀ (h₂ : l = k + 1 ∨ l < k + 1), l = k.succ ∨ l ≤ k
Tactic: rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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
k : ℕ
ih : ∀ {l : ℕ} (h₂ : l ≤ k), D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
rwa : ∀ (h₂ : l = k + 1 ∨ l < k + 1), l = k.succ ∨ l ≤ k
⊢ l = k.succ ∨ l ≤ k
have rwa₁ : ∀ (h₂ : l = k + 1 ∨ l ≤ k), l = k.succ ∨ l ≤ k
Tactic: rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (hypothesis)
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
k : ℕ
ih : ∀ {l : ℕ} (h₂ : l ≤ k), D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
⊢ D (k + 1) I ≤ D l J
have h : l = k.succ ∨ l ≤ k
Tactic: have h : l = k.succ ∨ l ≤ k := by rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
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
k : ℕ
ih : ∀ {l : ℕ} (h₂ : l ≤ k), D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
h : l = k.succ ∨ l ≤ k
⊢ D (k + 1) I ≤ D l J
have succ : ∀ (h : l = k.succ), D (k + 1) I ≤ D l J
Tactic: rcases h with h | h
Cleared hypotheses: h