awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 : R)
have 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)
Tactic: have := lie_e_pow_succ_toEnd_f P 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
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)
⊢ μ = (↑n : R)
have this₁ : 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
Cleared hypotheses: this
-- 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
P : t.HasPrimitiveVectorWith m μ
inst_7 : IsNoetherian R M
inst_8 : IsTorsionFree R M
inst_9 : IsDomain R
inst_10 : CharZero R
⊢ ∃ (n : ℕ), μ = (↑n : R)
have suffices : ∃ (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)
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
-- 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
P : t.HasPrimitiveVectorWith m μ
inst_7 : IsNoetherian R M
inst_8 : IsTorsionFree R M
inst_9 : IsDomain R
inst_10 : CharZero R
⊢ Set.Infinite.{u_1} (α := R) (range fun (n : ℕ) ↦ μ - HMul.hMul (α := R) 2 (↑n : R))
have rw : Infinite ℕ
Tactic: rw [infinite_range_iff (fun n m ↦ by simp)]
-- 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
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
⊢ ∃ (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)
have hs : Set.Infinite.{u_1} (α := R) (range fun (n : ℕ) ↦ μ - HMul.hMul (α := R) 2 (↑n : R))
Tactic: have hs : (range <| fun (n : ℕ) ↦ μ - 2 * n).Infinite := by
    rw [infinite_range_iff (fun n m ↦ by simp)]; infer_instance
-- 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
P : t.HasPrimitiveVectorWith m μ
inst_7 : IsNoetherian R M
inst_8 : IsTorsionFree R M
inst_9 : IsDomain R
inst_10 : CharZero R
hs : Set.Infinite.{u_1} (α := R) (range fun (n : ℕ) ↦ μ - HMul.hMul (α := R) 2 (↑n : R))
⊢ ∃ (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)
have by_contra! : ∀
  (contra :
    ∀ (n : ℕ),
      Ne (α := 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)),
  False
Tactic: by_contra! contra
-- 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
P : t.HasPrimitiveVectorWith m μ
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
i : ℕ
hi : i ≤ n
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)
            i :
          (a : M) → M)
        m :
      M)
    (0 : M)
⊢ False
have zero : ∀ (hi : 0 ≤ n)
  (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) 0 :
            (a : M) → M)
          m :
        M)
      (0 : M)),
  False
Tactic: induction i
Cleared hypotheses: i, hi, 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
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
i : ℕ
hi : i ≤ n
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)
            i :
          (a : M) → M)
        m :
      M)
    (0 : M)
zero :
  ∀ (hi : 0 ≤ n)
    (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) 0 :
              (a : M) → M)
            m :
          M)
        (0 : M)),
    False
⊢ False
have succ : ∀ (n_1 : ℕ),
  (∀ (hi : n_1 ≤ n)
      (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)),
      False) →
    ∀ (hi : n_1 + 1 ≤ n)
      (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 + 1) :
                (a : M) → M)
              m :
            M)
          (0 : M)),
      False
Tactic: induction i
Cleared hypotheses: i, hi, H
-- 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
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
i : ℕ
IH :
  ∀ (hi : i ≤ n)
    (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) i :
              (a : M) → M)
            m :
          M)
        (0 : M)),
    False
hi : i + 1 ≤ n
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)
            (i + 1) :
          (a : M) → M)
        m :
      M)
    (0 : M)
⊢ HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 * HSub.hSub (α := ℤ) (↑n : ℤ) (↑i : ℤ))
      ((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) i :
            (a : M) → M)
          m :
        M) =
    0
have this : Eq.{u_3 + 1} (α := M)
  ((fun (x : M) ↦ ⁅e, x⁆)
    ((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)
          (i + 1) :
        (a : M) → M)
      m))
  ((fun (x : M) ↦ ⁅e, x⁆) 0)
Tactic: have := congr_arg (⁅e, ·⁆) H
-- 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
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
i : ℕ
IH :
  ∀ (hi : i ≤ n)
    (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) i :
              (a : M) → M)
            m :
          M)
        (0 : M)),
    False
hi : i + 1 ≤ n
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)
            (i + 1) :
          (a : M) → M)
        m :
      M)
    (0 : M)
⊢ False
have this : HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 * HSub.hSub (α := ℤ) (↑n : ℤ) (↑i : ℤ))
    ((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)
            i :
          (a : M) → M)
        m :
      M) =
  0
Tactic: have : ((i + 1) * (n - i) : ℤ) • (toEnd R L M f ^ i) m = 0 := by
      have := congr_arg (⁅e, ·⁆) H
      simpa [← Int.cast_smul_eq_zsmul R, P.lie_e_pow_succ_toEnd_f, hn] using this
-- 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
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
i : ℕ
IH :
  ∀ (hi : i ≤ n)
    (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) i :
              (a : M) → M)
            m :
          M)
        (0 : M)),
    False
hi : i + 1 ≤ n
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)
            (i + 1) :
          (a : M) → M)
        m :
      M)
    (0 : M)
this :
  HSMul.hSMul (β := M) (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 * HSub.hSub (α := ℤ) (↑n : ℤ) (↑i : ℤ))
      ((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) i :
            (a : M) → M)
          m :
        M) =
    0
⊢ False
have this₁ : (i + 1 = 0 ∨ n = i) ∨
  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)
            i :
          (a : M) → M)
        m :
      M)
    (0 : M)
Tactic: rw [← Int.cast_smul_eq_zsmul R, smul_eq_zero, Int.cast_eq_zero, mul_eq_zero, sub_eq_zero,
      Nat.cast_inj, ← @Nat.cast_one ℤ, ← Nat.cast_add, Nat.cast_eq_zero] at this
Cleared hypotheses: this
-- 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
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
i : ℕ
IH :
  ∀ (hi : i ≤ n)
    (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) i :
              (a : M) → M)
            m :
          M)
        (0 : M)),
    False
hi : i + 1 ≤ n
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)
            (i + 1) :
          (a : M) → M)
        m :
      M)
    (0 : M)
this :
  (i + 1 = 0 ∨ n = i) ∨
    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) i :
            (a : M) → M)
          m :
        M)
      (0 : M)
⊢ False
have this₁ : n = i ∨
  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)
            i :
          (a : M) → M)
        m :
      M)
    (0 : M)
Tactic: simp only [add_eq_zero, one_ne_zero, and_false, false_or] at this
Cleared hypotheses: this
-- 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
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)
⊢ 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)
have by_contra : ∀
  (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)),
  False
Tactic: by_contra h
-- 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_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)
⊢ False
have 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)
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]) }
-- 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_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)
⊢ False
have obtain : ∀ (m : ℕ) (hm : (↑n : R) - 2 * HAdd.hAdd (α := R) (↑n : R) 1 = (↑m : R)), False
Tactic: obtain ⟨m, hm⟩ := this.exists_nat
-- 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_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)
⊢ False
have this₁ : (↑n : ℤ) < (↑m : ℤ) + 2 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
Tactic: have : (n : ℤ) < m + 2 * (n + 1) := by lia
-- 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 : ℕ
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)
have 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)
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]
-- 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 : ℕ
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)
⊢ 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)
have succ : 2 + (μ + HMul.hMul (α := R) 2 (↑n : R)) = μ + 2 * HAdd.hAdd (α := R) (↑n : R) 1
Tactic: congr 1