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
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 : HAdd.hAdd (α := R) (↑n : R) 1 = 0 ∨ μ = (↑n : R)
⊢ μ = (↑n : R)

Tactic:
this.resolve_left <| Nat.cast_add_one_ne_zero n

Premises used: Or.resolve_left, Nat.cast_add_one_ne_zero
-- 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
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 : HAdd.hAdd (α := R) (↑n : R) 1 = 0 ∨ μ = (↑n : R)
⊢ μ = (↑n : R)

Tactic:
exact this.resolve_left <| Nat.cast_add_one_ne_zero n

Premises used: Or.resolve_left, Nat.cast_add_one_ne_zero
-- 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
P : t.HasPrimitiveVectorWith m μ
inst_7 : IsNoetherian R M
inst_8 : IsTorsionFree R M
inst_9 : IsDomain R
inst_10 : CharZero R
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)
⊢ ∃ (n : ℕ), μ = (↑n : R)

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
-- 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_1 : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m_1 μ
inst_7 : IsNoetherian R M
inst_8 : IsTorsionFree R M
inst_9 : IsDomain R
inst_10 : CharZero R
n m : ℕ
⊢ μ - HMul.hMul (α := R) 2 (↑n : R) = μ - HMul.hMul (α := R) 2 (↑m : R) → n = m

Tactic:
simp
-- 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
P : t.HasPrimitiveVectorWith m μ
inst_7 : IsNoetherian R M
inst_8 : IsTorsionFree R M
inst_9 : IsDomain R
inst_10 : CharZero R
rw : Infinite ℕ
⊢ Set.Infinite.{u_1} (α := R) (range fun (n : ℕ) ↦ μ - HMul.hMul (α := R) 2 (↑n : R))

Tactic:
rw [infinite_range_iff (fun n m ↦ by simp)]

Premises used: Set.infinite_range_iff
-- 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
P : t.HasPrimitiveVectorWith m μ
inst_7 : IsNoetherian R M
inst_8 : IsTorsionFree R M
inst_9 : IsDomain R
inst_10 : CharZero R
⊢ Infinite ℕ

Tactic:
infer_instance
-- 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
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))

Tactic:
have hs : (range <| fun (n : ℕ) ↦ μ - 2 * n).Infinite := by
    rw [infinite_range_iff (fun n m ↦ by simp)]; infer_instance
-- 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
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))
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
⊢ ∃ (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:
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
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))
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)
x : (↑{x : R | ∃ (n : ℕ), μ - HMul.hMul (α := R) 2 (↑n : R) = x} : Type u_1)
r : R
hr : Membership.mem (γ := Set R) {x : R | ∃ (n : ℕ), μ - HMul.hMul (α := R) 2 (↑n : R) = x} r
⊢ End.HasEigenvector.{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)
    (↑(Subtype.mk (p := fun (x : R) ↦
          Membership.mem (γ := Set R) {x : R | ∃ (n : ℕ), μ - HMul.hMul (α := R) 2 (↑n : R) = x} x) r hr) :
      R)
    ((fun (x : (↑{x : R | ∃ (n : ℕ), μ - HMul.hMul (α := R) 2 (↑n : R) = x} : Type u_1)) ↦
        (match (motive := (↑{x : R | ∃ (n : ℕ), μ - HMul.hMul (α := R) 2 (↑n : R) = x} : Type u_1) → M) x with
          | ⟨s, hs⟩ =>
            (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)
                  (Classical.choose (p := fun (x : ℕ) ↦ μ - HMul.hMul (α := R) 2 (↑x : R) = s) hs) :
                (a : M) → M)
              m :
          M))
      (Subtype.mk (p := fun (x : R) ↦
        Membership.mem (γ := Set R) {x : R | ∃ (n : ℕ), μ - HMul.hMul (α := R) 2 (↑n : R) = x} x) r hr))

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

Premises used: Module.End.hasEigenvector_iff, Classical.choose_spec, IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f
-- 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
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))
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:
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])).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
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
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
⊢ False

Tactic:
induction i
-- 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
P : t.HasPrimitiveVectorWith m μ
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
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)
⊢ m = 0

Tactic:
simpa using H
-- 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
P : t.HasPrimitiveVectorWith m μ
inst_7 : CharZero R
inst_8 : IsDomain R
inst_9 : IsTorsionFree R M
n : ℕ
hn : μ = (↑n : R)
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:
exact P.ne_zero (by simpa using H)

Premises used: IsSl2Triple.HasPrimitiveVectorWith.ne_zero
-- 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
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)
⊢ 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
-- 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
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 :
  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)
⊢ 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:
simpa [← Int.cast_smul_eq_zsmul R, P.lie_e_pow_succ_toEnd_f, hn] using this

Premises used: IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f, Int.cast_smul_eq_zsmul
-- 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
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

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
-- 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
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
⊢ (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

Premises used: sub_eq_zero, Nat.cast_inj, mul_eq_zero, Nat.cast_add, Nat.cast_eq_zero, Int.cast_eq_zero, Nat.cast_one, Int.cast_smul_eq_zsmul, smul_eq_zero
-- 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
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)
⊢ 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

Premises used: false_or, and_false, add_eq_zero, one_ne_zero
-- 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
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 :
  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

Tactic:
(hi.trans_eq (this.resolve_right (IH (i.le_succ.trans hi)))).not_gt i.lt_succ_self

Premises used: LE.le.trans_eq, Nat.lt_succ_self, Nat.le_succ, LE.le.not_gt, Or.resolve_right, LE.le.trans
-- 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
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 :
  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

Tactic:
exact (hi.trans_eq (this.resolve_right (IH (i.le_succ.trans hi)))).not_gt i.lt_succ_self

Premises used: LE.le.trans_eq, Nat.lt_succ_self, Nat.le_succ, LE.le.not_gt, Or.resolve_right, LE.le.trans
-- 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
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)
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
⊢ 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)

Tactic:
by_contra h