awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
refine :
  Eq (α := L → A)
      (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
        (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
      (⇑f : (a : L) → A) ↔
    (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g = f
⊢ Eq (α := L → A)
      (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
        (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
      (⇑f : (a : L) → A) ↔
    g = (lift R : (a : L →ₗ⁅R⁆ A) → UniversalEnvelopingAlgebra R L →ₐ[R] A) f

Tactic:
refine Iff.trans ?_ (lift R).symm_apply_eq

Premises used: UniversalEnvelopingAlgebra.lift, Equiv.symm_apply_eq, Iff.trans
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
mp :
  Eq (α := L → A)
      (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
        (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
      (⇑f : (a : L) → A) →
    (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g = f
mpr :
  (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g = f →
    Eq (α := L → A)
      (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
        (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
      (⇑f : (a : L) → A)
⊢ Eq (α := L → A)
      (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
        (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
      (⇑f : (a : L) → A) ↔
    (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g = f

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h :
  Eq (α := L → A)
    (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
      (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
    (⇑f : (a : L) → A)
mp :
  ∀ (x : L),
    Eq.{u₃ + 1} (α := A)
      ((((Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g : L →ₗ⁅R⁆ A) : (a : L) → A)
          x :
        A)
      ((f : (a : L) → A) x : A)
⊢ (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g = f

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h :
  Eq (α := L → A)
    (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
      (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
    (⇑f : (a : L) → A)
x : L
⊢ Eq.{u₃ + 1} (α := A)
    ((((Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g : L →ₗ⁅R⁆ A) : (a : L) → A)
        x :
      A)
    ((f : (a : L) → A) x : A)

Tactic:
simp [← h]
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g = f
mpr :
  ∀ (x : L),
    Eq.{u₃ + 1} (α := A)
      (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
          (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L) x :
        A)
      ((f : (a : L) → A) x : A)
⊢ Eq (α := L → A)
    (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
      (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L))
    (⇑f : (a : L) → A)

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
f : L →ₗ⁅R⁆ A
g : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : (Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g = f
x : L
⊢ Eq.{u₃ + 1} (α := A)
    (Function.comp (β := UniversalEnvelopingAlgebra R L) (⇑g : (a : UniversalEnvelopingAlgebra R L) → A)
        (⇑(ι R) : (a : L) → UniversalEnvelopingAlgebra R L) x :
      A)
    ((f : (a : L) → A) x : A)

Tactic:
simp [← h]
-- Module: Mathlib.Algebra.Lie.UniversalEnveloping
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
A : Type u₃
inst_3 : Ring A
inst_4 : Algebra R A
g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : g₁.toLieHom.comp (ι R) = g₂.toLieHom.comp (ι R)
⊢ Eq (α := L →ₗ⁅R⁆ A) ((Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g₁ : L →ₗ⁅R⁆ A)
    ((Equiv.symm (lift R) : (a : UniversalEnvelopingAlgebra R L →ₐ[R] A) → L →ₗ⁅R⁆ A) g₂ : L →ₗ⁅R⁆ A)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing.IsNilpotent L
⊢ Eq.{u_2 + 1} (α := LieSubmodule R (↥⊤) L) (rootSpace ⊤ 0) ⊤

Tactic:
zero_genWeightSpace_eq_top_of_nilpotent L

Premises used: LieModule.zero_genWeightSpace_eq_top_of_nilpotent
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
χ : ↥H → R
⊢ LieSubmodule.comap H.incl' (rootSpace H χ) = genWeightSpace (↥H) χ

Tactic:
comap_genWeightSpace_eq_of_injective Subtype.coe_injective

Premises used: Subtype.coe_injective, LieModule.comap_genWeightSpace_eq_of_injective
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
rw :
  ∀ (i : ↥H),
    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
      (genWeightSpaceOf M ((χ₁ + χ₂) i) i : LieSubmodule.{u_1, u_2, u_3} R (↥H) M) ⁅x, m⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (χ₁ + χ₂)) ⁅x, m⁆

Tactic:
rw [genWeightSpace, LieSubmodule.mem_iInf]

Premises used: LieSubmodule.mem_iInf, LieModule.genWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
y : ↥H
rw :
  ∀ (hx : ∀ (i : ↥H), Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ i) i) x)
    (hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m) (y : ↥H),
    Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x
⊢ Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x

Tactic:
rw [rootSpace, genWeightSpace, LieSubmodule.mem_iInf] at hx

Premises used: LieSubmodule.mem_iInf, LieAlgebra.rootSpace, LieModule.genWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : ∀ (i : ↥H), Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ i) i) x
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
y : ↥H
⊢ Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x

Tactic:
hx y

Premises used: Set.Mem, setOf
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : ∀ (i : ↥H), Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ i) i) x
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
y : ↥H
⊢ Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x

Tactic:
exact hx y
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
y : ↥H
⊢ Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x

Tactic:
replace hx : x ∈ genWeightSpaceOf L (χ₁ y) y := by
    rw [rootSpace, genWeightSpace, LieSubmodule.mem_iInf] at hx; exact hx y
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
y : ↥H
hx : Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x
rw :
  ∀ (hm : ∀ (i : ↥H), Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceOf M (χ₂ i) i) m)
    (y : ↥H) (hx : Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x),
    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceOf M (χ₂ y) y) m
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceOf M (χ₂ y) y) m

Tactic:
rw [genWeightSpace, LieSubmodule.mem_iInf] at hm

Premises used: LieSubmodule.mem_iInf, LieModule.genWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hm : ∀ (i : ↥H), Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceOf M (χ₂ i) i) m
y : ↥H
hx : Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceOf M (χ₂ y) y) m

Tactic:
hm y
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hm : ∀ (i : ↥H), Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceOf M (χ₂ i) i) m
y : ↥H
hx : Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceOf M (χ₂ y) y) m

Tactic:
exact hm y
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
y : ↥H
hx : Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceOf M (χ₂ y) y) m

Tactic:
replace hm : m ∈ genWeightSpaceOf M (χ₂ y) y := by
    rw [genWeightSpace, LieSubmodule.mem_iInf] at hm; exact hm y
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
y : ↥H
hx : Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceOf M (χ₂ y) y) m
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpaceOf M ((χ₁ + χ₂) y) y : LieSubmodule.{u_1, u_2, u_3} R (↥H) M) ⁅x, m⁆

Tactic:
lie_mem_maxGenEigenspace_toEnd hx hm

Premises used: Set.Mem, setOf, LieModule.lie_mem_maxGenEigenspace_toEnd
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
y : ↥H
hx : Membership.mem (γ := LieSubmodule R (↥H) L) (genWeightSpaceOf L (χ₁ y) y) x
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceOf M (χ₂ y) y) m
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpaceOf M ((χ₁ + χ₂) y) y : LieSubmodule.{u_1, u_2, u_3} R (↥H) M) ⁅x, m⁆

Tactic:
exact lie_mem_maxGenEigenspace_toEnd hx hm

Premises used: LieModule.lie_mem_maxGenEigenspace_toEnd
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
⊢ Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpace M (HSMul.hSMul (α := ℕ) 0 χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M) (β := ℕ)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            0 :
          (a : M) → M)
        m :
      M)

Tactic:
simpa using hm
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
n : ℕ
IH :
  Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (n • χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            n :
          (a : M) → M)
        m :
      M)
succ :
  Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((n + 1) • χ₁ + χ₂))
    (⁅x,
        (HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              n :
            (a : M) → M)
          m⁆ :
      M)
⊢ Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((n + 1) • χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            (n + 1) :
          (a : M) → M)
        m :
      M)

Tactic:
simp only [pow_succ', Module.End.mul_apply, toEnd_apply_apply]

Premises used: LieModule.toEnd_apply_apply, Module.End.mul_apply, pow_succ'
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
n : ℕ
IH :
  Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (n • χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            n :
          (a : M) → M)
        m :
      M)
h : (n + 1) • χ₁ + χ₂ = χ₁ + (n • χ₁ + χ₂)
⊢ Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((n + 1) • χ₁ + χ₂))
    (⁅x,
        (HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              n :
            (a : M) → M)
          m⁆ :
      M)

Tactic:
convert! lie_mem_genWeightSpace_of_mem_genWeightSpace hx IH using 2

Premises used: LieAlgebra.lie_mem_genWeightSpace_of_mem_genWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
n : ℕ
IH :
  Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (n • χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            n :
          (a : M) → M)
        m :
      M)
h : n • χ₁ + χ₁ + χ₂ = χ₁ + (n • χ₁ + χ₂)
h₁ : n • χ₁ + χ₁ + χ₂ = χ₁ + n • χ₁ + χ₂
h₂ h₃ : χ₁ + n • χ₁ + χ₂ = χ₁ + n • χ₁ + χ₂
⊢ (n + 1) • χ₁ + χ₂ = χ₁ + (n • χ₁ + χ₂)

Tactic:
rw [succ_nsmul, ← add_assoc, add_comm (n • _)]

Premises used: add_assoc, add_comm, HSMul.hSMul, succ_nsmul
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₂) m
n : ℕ
zero :
  Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (genWeightSpace M (HSMul.hSMul (α := ℕ) 0 χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M) (β := ℕ)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            0 :
          (a : M) → M)
        m :
      M)
succ :
  ∀ (n : ℕ)
    (IH :
      Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (n • χ₁ + χ₂))
        ((HPow.hPow (α := Module.End R M)
                (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                  Module.End R M)
                n :
              (a : M) → M)
            m :
          M)),
    Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((n + 1) • χ₁ + χ₂))
      ((HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              (n + 1) :
            (a : M) → M)
          m :
        M)
⊢ Membership.mem (α := M) (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (n • χ₁ + χ₂))
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x :
              Module.End R M)
            n :
          (a : M) → M)
        m :
      M)

Tactic:
induction n with
  | zero => simpa using hm
  | succ n IH =>
    simp only [pow_succ', Module.End.mul_apply, toEnd_apply_apply]
    convert! lie_mem_genWeightSpace_of_mem_genWeightSpace hx IH using 2
    rw [succ_nsmul, ← add_assoc, add_comm (n • _)]

Premises used: add_assoc, add_comm, LieModule.toEnd_apply_apply, HSMul.hSMul, Module.End.mul_apply, pow_succ', succ_nsmul
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) m
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ)
    (Bracket.bracket.{u_2, u_3} (L := L) 0 m)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) m
x_1 y : L
hx : Membership.mem (γ := LieSubmodule R (↥H) L) (⨆ i ∈ s, rootSpace H i) x_1
hy : Membership.mem (γ := LieSubmodule R (↥H) L) (⨆ i ∈ s, rootSpace H i) y
hu : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅x_1, m⁆
hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅y, m⁆
add : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) (⁅x_1, m⁆ + ⁅y, m⁆)
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅x_1 + y, m⁆

Tactic:
rw [add_lie]

Premises used: add_lie