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
t : IsSl2Triple h e f
x y : L
hx : Membership.mem (γ := Submodule R L) (span R {e, f, h}) x
hy : Membership.mem (γ := Submodule R L) (span R {e, f, h}) y
zero : Membership.mem (γ := Submodule R L) (span R {e, f, h}) (Bracket.bracket (L := L) 0 y)
add :
  ∀ (u v : L) (hu : Membership.mem (γ := Submodule R L) (span R {e, f, h}) u)
    (hv : Membership.mem (γ := Submodule R L) (span R {e, f, h}) v)
    (hu' : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, y⁆)
    (hv' : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅v, y⁆),
    Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u + v, y⁆
smul :
  ∀ (t : R) (u : L) (hu : Membership.mem (γ := Submodule R L) (span R {e, f, h}) u)
    (hu' : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, y⁆),
    Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅t • u, y⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅x, y⁆
have mem : ∀ (u : L) (hu : Membership.mem (γ := Set L) {e, f, h} u), Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, y⁆
Tactic: induction hx using span_induction with
    | zero => simp
    | add u v hu hv hu' hv' => simpa only [add_lie] using add_mem hu' hv'
    | smul t u hu hu' => simpa only [smul_lie] using smul_mem _ t hu'
    | mem u hu =>
      induction hy using span_induction with
      | zero => simp
      | add u v hu hv hu' hv' => simpa only [lie_add] using add_mem hu' hv'
      | smul t u hv hv' => simpa only [lie_smul] using smul_mem _ t hv'
      | mem v hv =>
        push _ ∈ _ at hu hv
        rcases hu with rfl | rfl | rfl <;>
        rcases hv with rfl | rfl | rfl <;> (try simp only [lie_self, zero_mem])
        · rw [t.lie_e_f]
          apply subset_span
          simp
        · rw [← lie_skew, t.lie_h_e_nsmul, neg_mem_iff]
          apply nsmul_mem <| subset_span _
          simp
        · rw [← lie_skew, t.lie_e_f, neg_mem_iff]
          apply subset_span
          simp
        · rw [← lie_skew, t.lie_h_f_nsmul, neg_neg]
          apply nsmul_mem <| subset_span _
          simp
        · rw [t.lie_h_e_nsmul]
          apply nsmul_mem <| subset_span _
          simp
        · rw [t.lie_h_f_nsmul, neg_mem_iff]
          apply nsmul_mem <| subset_span _
          simp
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h e f x : L
t : IsSl2Triple h e f
⊢ Membership.mem (γ := LieSubalgebra R L) (toLieSubalgebra R t) x ↔
    ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
have simp_rw : Membership.mem (γ := LieSubalgebra R L) (toLieSubalgebra R t) x ↔
  ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • h
Tactic: simp_rw [t.lie_e_f, toLieSubalgebra, ← LieSubalgebra.mem_toSubmodule, Submodule.mem_span_triple,
    eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h e f x : L
t : IsSl2Triple h e f
simp_rw :
  Membership.mem (γ := LieSubalgebra R L) (toLieSubalgebra R t) x ↔
    ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • h
⊢ Membership.mem (γ := LieSubalgebra R L) (toLieSubalgebra R t) x ↔
    ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
have simp_rw₁ : Membership.mem (γ := LieSubalgebra R L) { toSubmodule := Submodule.span R {e, f, h}, lie_mem' := sorry } x ↔
  ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • h
Tactic: simp_rw [t.lie_e_f, toLieSubalgebra, ← LieSubalgebra.mem_toSubmodule, Submodule.mem_span_triple,
    eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h e f x : L
t : IsSl2Triple h e f
simp_rw :
  Membership.mem (γ := LieSubalgebra R L) (toLieSubalgebra R t) x ↔
    ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • h
simp_rw₁ :
  Membership.mem (γ := LieSubalgebra R L) { toSubmodule := Submodule.span R {e, f, h}, lie_mem' := ⋯ } x ↔
    ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • h
⊢ Membership.mem (γ := LieSubalgebra R L) (toLieSubalgebra R t) x ↔
    ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
have simp_rw₂ : Membership.mem (γ := Submodule R L) (Submodule.span R {e, f, h}) x ↔
  ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • h
Tactic: simp_rw [t.lie_e_f, toLieSubalgebra, ← LieSubalgebra.mem_toSubmodule, Submodule.mem_span_triple,
    eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Sl2 (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h e f x : L
t : IsSl2Triple h e f
simp_rw :
  Membership.mem (γ := LieSubalgebra R L) (toLieSubalgebra R t) x ↔
    ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • h
simp_rw₁ :
  Membership.mem (γ := LieSubalgebra R L) { toSubmodule := Submodule.span R {e, f, h}, lie_mem' := ⋯ } x ↔
    ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • h
simp_rw₂ :
  Membership.mem (γ := Submodule R L) (Submodule.span R {e, f, h}) x ↔
    ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • h
⊢ Membership.mem (γ := LieSubalgebra R L) (toLieSubalgebra R t) x ↔
    ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
have simp_rw₃ : (∃ (a : R) (b : R) (c : R), a • e + b • f + c • h = x) ↔ ∃ (c₁ : R) (c₂ : R) (c₃ : R), x = c₁ • e + c₂ • f + c₃ • h
Tactic: simp_rw [t.lie_e_f, toLieSubalgebra, ← LieSubalgebra.mem_toSubmodule, Submodule.mem_span_triple,
    eq_comm]
-- 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 μ
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) f : 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) f : 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) f : 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) f : End R M) (n + 1) :
            (a : M) → M)
          m :
        M)
have succ : HSMul.hSMul (β := M) (-2 + (μ - HMul.hMul (α := R) 2 (↑n : R)))
    (⁅f,
        (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) =
  HSMul.hSMul (β := M) (μ - 2 * HAdd.hAdd (α := R) (↑n : R) 1)
    (⁅f,
        (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: rw [pow_succ', Module.End.mul_apply, toEnd_apply_apply, Nat.cast_add, Nat.cast_one,
      leibniz_lie h, t.lie_lie_smul_f R, ← neg_smul, ih, lie_smul, smul_lie, ← 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
P : t.HasPrimitiveVectorWith 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) f : 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) f : End R M) n :
            (a : M) → M)
          m :
        M)
⊢ HSMul.hSMul (β := M) (-2 + (μ - HMul.hMul (α := R) 2 (↑n : R)))
      (⁅f,
          (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) =
    HSMul.hSMul (β := M) (μ - 2 * HAdd.hAdd (α := R) (↑n : R) 1)
      (⁅f,
          (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)
have succ : -2 + (μ - HMul.hMul (α := R) 2 (↑n : R)) = μ - 2 * HAdd.hAdd (α := R) (↑n : R) 1
Tactic: congr
-- 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 μ
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) f : 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) f : 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) f : 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) f : End R M) 0 :
          (a : M) → M)
        m :
      M)
Tactic: induction n with
  | zero => simpa using P.lie_h
  | succ n ih =>
    rw [pow_succ', Module.End.mul_apply, toEnd_apply_apply, Nat.cast_add, Nat.cast_one,
      leibniz_lie h, t.lie_lie_smul_f R, ← neg_smul, ih, lie_smul, smul_lie, ← add_smul]
    congr
    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
P : t.HasPrimitiveVectorWith 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) f : 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) f : 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) f : 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) f : 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) f : 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) f : 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) f : 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) f : End R M) (n + 1) :
            (a : M) → M)
          m :
        M)
Tactic: induction n with
  | zero => simpa using P.lie_h
  | succ n ih =>
    rw [pow_succ', Module.End.mul_apply, toEnd_apply_apply, Nat.cast_add, Nat.cast_one,
      leibniz_lie h, t.lie_lie_smul_f R, ← neg_smul, ih, lie_smul, smul_lie, ← add_smul]
    congr
    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
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih :
  ⁅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)
⊢ ⁅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 + 1) :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (HAdd.hAdd (α := R) (↑(n + 1) : R) 1 * (μ - (↑(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) f : End R M) (n + 1) :
            (a : M) → M)
          m :
        M)
have succ : HSMul.hSMul (β := M) (μ - 2 * HAdd.hAdd (α := R) (↑n : R) 1 + 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 + 1) :
          (a : M) → M)
        m :
      M) =
  HSMul.hSMul (β := M) ((HAdd.hAdd (α := R) (↑n : R) 1 + 1) * (μ - HAdd.hAdd (α := R) (↑n : R) 1))
    ((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)
Tactic: rw [pow_succ', Module.End.mul_apply, toEnd_apply_apply, leibniz_lie e, t.lie_e_f,
      lie_h_pow_toEnd_f P, ih, lie_smul, lie_f_pow_toEnd_f P, ← add_smul,
      Nat.cast_add, Nat.cast_one]
-- 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 μ
n : ℕ
ih :
  ⁅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)
⊢ HSMul.hSMul (β := M) (μ - 2 * HAdd.hAdd (α := R) (↑n : R) 1 + 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 + 1) :
            (a : M) → M)
          m :
        M) =
    HSMul.hSMul (β := M) ((HAdd.hAdd (α := R) (↑n : R) 1 + 1) * (μ - HAdd.hAdd (α := R) (↑n : R) 1))
      ((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)
have succ : μ - 2 * HAdd.hAdd (α := R) (↑n : R) 1 + HAdd.hAdd (α := R) (↑n : R) 1 * (μ - (↑n : R)) =
  (HAdd.hAdd (α := R) (↑n : R) 1 + 1) * (μ - HAdd.hAdd (α := R) (↑n : R) 1)
Tactic: congr
-- 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 μ
n : ℕ
⊢ ⁅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)
have zero : ⁅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)
          (HAdd.hAdd (α := ℕ) 0 1) :
        (a : M) → M)
      m⁆ =
  HSMul.hSMul (β := M) (HAdd.hAdd (α := R) (↑0 : R) 1 * (μ - (↑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) f : End R M) 0 :
          (a : M) → M)
        m :
      M)
Tactic: induction n with
  | zero =>
      simp only [zero_add, pow_one, toEnd_apply_apply, Nat.cast_zero, sub_zero, one_mul,
        pow_zero, Module.End.one_apply, leibniz_lie e, t.lie_e_f, P.lie_e, P.lie_h, lie_zero,
        add_zero]
  | succ n ih =>
    rw [pow_succ', Module.End.mul_apply, toEnd_apply_apply, leibniz_lie e, t.lie_e_f,
      lie_h_pow_toEnd_f P, ih, lie_smul, lie_f_pow_toEnd_f P, ← add_smul,
      Nat.cast_add, Nat.cast_one]
    congr
    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
P : t.HasPrimitiveVectorWith m μ
n : ℕ
zero :
  ⁅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)
            (HAdd.hAdd (α := ℕ) 0 1) :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (HAdd.hAdd (α := R) (↑0 : R) 1 * (μ - (↑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) f : End R M) 0 :
            (a : M) → M)
          m :
        M)
⊢ ⁅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)
have succ : ∀ (n : ℕ)
  (ih :
    ⁅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)),
  ⁅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 + 1) :
          (a : M) → M)
        m⁆ =
    HSMul.hSMul (β := M) (HAdd.hAdd (α := R) (↑(n + 1) : R) 1 * (μ - (↑(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) f : End R M) (n + 1) :
            (a : M) → M)
          m :
        M)
Tactic: induction n with
  | zero =>
      simp only [zero_add, pow_one, toEnd_apply_apply, Nat.cast_zero, sub_zero, one_mul,
        pow_zero, Module.End.one_apply, leibniz_lie e, t.lie_e_f, P.lie_e, P.lie_h, lie_zero,
        add_zero]
  | succ n ih =>
    rw [pow_succ', Module.End.mul_apply, toEnd_apply_apply, leibniz_lie e, t.lie_e_f,
      lie_h_pow_toEnd_f P, ih, lie_smul, lie_f_pow_toEnd_f P, ← add_smul,
      Nat.cast_add, Nat.cast_one]
    congr
    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
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 : ℕ), μ = (↑n : R)
have obtain : ∀ (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 : ℕ), μ = (↑n : R)
Tactic: obtain ⟨n, hn₁, hn₂⟩ := Nat.exists_not_and_succ_of_not_zero_of_exists P.ne_zero 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
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 : ℕ), μ = (↑n : R)
have refine : μ = (↑n : R)
Tactic: refine ⟨n, ?_⟩