-- Mathlib/Algebra/Lie/Weights/Cartan.lean
theorem mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace (α χ : H → R)
    {x : L} (hx : x ∈ rootSpace H α) :
    MapsTo (toEnd R L M x) (genWeightSpace M χ) (genWeightSpace M (α + χ))

Proof state:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
α χ : ↥H → R
x : L
hx : x ∈ rootSpace H α
m : M
hm : m ∈ ↑(genWeightSpace M χ)
x' : ↥(rootSpace H α) := ⟨x, hx⟩
m' : ↥(genWeightSpace M χ) := ⟨m, hm⟩
⊢ ((toEnd R L M) x) m ∈ ↑(genWeightSpace M (α + χ))

Tactic:
exact (rootSpaceWeightSpaceProduct R L H M α χ (α + χ) rfl (x' ⊗ₜ m')).property

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
α χ : ↥H → R
x : L
hx : x ∈ rootSpace H α
m : M
hm : m ∈ ↑(genWeightSpace M χ)
x' : ↥(rootSpace H α) := ⟨x, hx⟩
⊢ ((toEnd R L M) x) m ∈ ↑(genWeightSpace M (α + χ))

Tactic:
let m' : genWeightSpace M χ := ⟨m, hm⟩

Result:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
α χ : ↥H → R
x : L
hx : x ∈ rootSpace H α
m : M
hm : m ∈ ↑(genWeightSpace M χ)
x' : ↥(rootSpace H α) := ⟨x, hx⟩
m' : ↥(genWeightSpace M χ) := ⟨m, hm⟩
⊢ ((toEnd R L M) x) m ∈ ↑(genWeightSpace M (α + χ))

Proof state:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
α χ : ↥H → R
x : L
hx : x ∈ rootSpace H α
⊢ MapsTo ⇑((toEnd R L M) x) ↑(genWeightSpace M χ) ↑(genWeightSpace M (α + χ))

Tactic:
intro m hm

Result:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
α χ : ↥H → R
x : L
hx : x ∈ rootSpace H α
m : M
hm : m ∈ ↑(genWeightSpace M χ)
⊢ ((toEnd R L M) x) m ∈ ↑(genWeightSpace M (α + χ))

Proof state:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
α χ : ↥H → R
x : L
hx : x ∈ rootSpace H α
m : M
hm : m ∈ ↑(genWeightSpace M χ)
⊢ ((toEnd R L M) x) m ∈ ↑(genWeightSpace M (α + χ))

Tactic:
let x' : rootSpace H α := ⟨x, hx⟩

Result:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
α χ : ↥H → R
x : L
hx : x ∈ rootSpace H α
m : M
hm : m ∈ ↑(genWeightSpace M χ)
x' : ↥(rootSpace H α) := ⟨x, hx⟩
⊢ ((toEnd R L M) x) m ∈ ↑(genWeightSpace M (α + χ))