mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
this✝ : FiniteDimensional K ↥K⟮x⟯
this : FiniteDimensional K ↥K⟮y⟯
⊢ FiniteDimensional K ↥(K⟮x⟯ ⊔ K⟮y⟯)

Tactic:
]

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
this✝ : FiniteDimensional K ↥K⟮x⟯
this : FiniteDimensional K ↥K⟮y⟯
⊢ FiniteDimensional K ↥(K⟮x⟯ ⊔ K⟮y⟯)
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: L : Type u_2
inst✝ : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ h = h

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: L : Type u_2
inst✝ : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ -(2 • f) = -(2 • f)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: L : Type u_2
inst✝ : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ 2 • e = 2 • e

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
⊢ H.toSubmodule = H.toSubmodule

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.IsCartanSubalgebra
h₁ : LieRing.IsNilpotent ↥H
k : ℕ
hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥
l : ℕ
hl : k ≤ l
⊢ H.toLieSubmodule = H.toLieSubmodule

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
⊢ ∃ k, LieSubmodule.lcs k H.toLieSubmodule = ⊥

Tactic:
]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
⊢ ∃ k, LieSubmodule.lcs k H.toLieSubmodule = ⊥
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
⊢ H.toLieSubmodule ≤ H.toLieSubmodule

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
hk' : H.toLieSubmodule.normalizer = H.toLieSubmodule
⊢ H.normalizer = H

Tactic:
]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
hk' : H.toLieSubmodule.normalizer = H.toLieSubmodule
⊢ H.normalizer = H
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
ih : ∀ (φ : K), ⨆ χ, ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤
φ : K
χ : ι → K
hχ : χ i ≠ φ
⊢ Disjoint ((f i).maxGenEigenspace φ) (⨅ i, (f i).maxGenEigenspace (χ i))

Tactic:
]

Goal state after:
ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
ih : ∀ (φ : K), ⨆ χ, ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤
φ : K
χ : ι → K
hχ : χ i ≠ φ
⊢ Disjoint ((f i).maxGenEigenspace φ) (⨅ i, (f i).maxGenEigenspace (χ i))
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
h e f : L
inst✝ : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
hk' : H.toLieSubmodule.normalizer = H.toLieSubmodule
⊢ H.toSubmodule = H.toSubmodule

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
this : x ∈ ⊥
⊢ x = 0

Tactic:
]

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
this : x ∈ ⊥
⊢ x = 0
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H✝ : LieSubalgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
inst : Subsingleton ↥H
⊢ ∀ x ∈ H, x = 0

Tactic:
]

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H✝ : LieSubalgebra R L
inst✝¹ : Nontrivial L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
inst : Subsingleton ↥H
⊢ ∀ x ∈ H, x = 0
Module: Mathlib.Algebra.Lie.CartanSubalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent L
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝³ : Field K
n : ℕ
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : ∀ (i j : ι) (φ : K), MapsTo ⇑(f i) ↑((f j).maxGenEigenspace φ) ↑((f j).maxGenEigenspace φ)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
h_dim : finrank K M = n
i : ι
hy : ∀ (φ : K), finrank K ↥((f i).maxGenEigenspace φ) < n
hi : ∀ (j : ι) (φ : K), MapsTo ⇑(f j) ↑((f i).maxGenEigenspace φ) ↑((f i).maxGenEigenspace φ)
ih : ∀ (φ : K), ⨆ χ, ⨆ (_ : χ i = φ), ⨅ j, maxGenEigenspace (LinearMap.restrict (f j) ⋯) (χ j) = ⊤
φ : K
χ : ι → K
hχ : χ i = φ
⊢ ⨅ j, (f j).maxGenEigenspace (χ j) = ⨅ j, (f j).maxGenEigenspace (χ j)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: case h
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
m₁ : M₁
hm₁ : m₁ ∈ 𝕎(M₁, χ₁, x)
m₂ : M₂
hm₂ : m₂ ∈ 𝕎(M₂, χ₂, x)
f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)
f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)
h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)
k : ℕ
hk : ((f₁ + f₂) ^ k) (m₁ ⊗ₜ[R] m₂) = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: 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
m : M
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
⊢ ∀ (i : ↥H), ⁅x, m⁆ ∈ genWeightSpaceOf M ((χ₁ + χ₂) i) i

Tactic:
]

Goal state after:
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
m : M
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
⊢ ∀ (i : ↥H), ⁅x, m⁆ ∈ genWeightSpaceOf M ((χ₁ + χ₂) i) i
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: 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
m : M
hx : ∀ (i : ↥H), x ∈ genWeightSpaceOf L (χ₁ i) i
hm : m ∈ genWeightSpace M χ₂
y : ↥H
⊢ x ∈ genWeightSpaceOf L (χ₁ y) y

Tactic:
]

Goal state after:
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
m : M
hx : ∀ (i : ↥H), x ∈ genWeightSpaceOf L (χ₁ i) i
hm : m ∈ genWeightSpace M χ₂
y : ↥H
⊢ x ∈ genWeightSpaceOf L (χ₁ y) y
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: 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
m : M
hm : ∀ (i : ↥H), m ∈ genWeightSpaceOf M (χ₂ i) i
y : ↥H
hx : x ∈ genWeightSpaceOf L (χ₁ y) y
⊢ m ∈ genWeightSpaceOf M (χ₂ y) y

Tactic:
]

Goal state after:
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
m : M
hm : ∀ (i : ↥H), m ∈ genWeightSpaceOf M (χ₂ i) i
y : ↥H
hx : x ∈ genWeightSpaceOf L (χ₁ y) y
⊢ m ∈ genWeightSpaceOf M (χ₂ y) y
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case mem.mem.inl.inr.inl
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h x y u v : L
t : IsSl2Triple h u v
__spread✝⁻⁰ : Submodule R L := span R {u, v, h}
⊢ h ∈ span R {u, v, h}

Tactic:
]

Goal state after:
case mem.mem.inl.inr.inl
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h x y u v : L
t : IsSl2Triple h u v
__spread✝⁻⁰ : Submodule R L := span R {u, v, h}
⊢ h ∈ span R {u, v, h}
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: 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
m : M
y : ↥H
hx : x ∈ genWeightSpaceOf L (χ₁ y) y
hm : m ∈ genWeightSpaceOf M (χ₂ y) y
⊢ ⁅x, m⁆ ∈ genWeightSpaceOf M ((χ₁ + χ₂) y) y

Tactic:
exact lie_mem_maxGenEigenspace_toEnd hx hm

Goal state after:
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case mem.mem.inl.inr.inr
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
f x y u v : L
t : IsSl2Triple v u f
__spread✝⁻⁰ : Submodule R L := span R {u, f, v}
⊢ 2 • u ∈ span R {u, f, v}

Tactic:
]

Goal state after:
case mem.mem.inl.inr.inr
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
f x y u v : L
t : IsSl2Triple v u f
__spread✝⁻⁰ : Submodule R L := span R {u, f, v}
⊢ 2 • u ∈ span R {u, f, v}
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case mem.mem.inr.inl.inl
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h x y u v : L
t : IsSl2Triple h v u
__spread✝⁻⁰ : Submodule R L := span R {v, u, h}
⊢ h ∈ span R {v, u, h}

Tactic:
]

Goal state after:
case mem.mem.inr.inl.inl
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h x y u v : L
t : IsSl2Triple h v u
__spread✝⁻⁰ : Submodule R L := span R {v, u, h}
⊢ h ∈ span R {v, u, h}
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case mem.mem.inr.inl.inr.inr
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
e x y u v : L
t : IsSl2Triple v e u
__spread✝⁻⁰ : Submodule R L := span R {e, u, v}
⊢ 2 • u ∈ span R {e, u, v}

Tactic:
]

Goal state after:
case mem.mem.inr.inl.inr.inr
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
e x y u v : L
t : IsSl2Triple v e u
__spread✝⁻⁰ : Submodule R L := span R {e, u, v}
⊢ 2 • u ∈ span R {e, u, v}
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: case h
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)
f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)
h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0
k₂ : ℕ
hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0
hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0
hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0
hf_comm : Commute f₁ f₂
⊢ (∑ m ∈ Finset.antidiagonal (k₁ + k₂ - 1), (k₁ + k₂ - 1).choose m.1 • (f₁ ^ m.1 * f₂ ^ m.2)) (m₁ ⊗ₜ[R] m₂) = 0

Tactic:
]

Goal state after:
case h
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)
f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)
h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0
k₂ : ℕ
hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0
hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0
hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0
hf_comm : Commute f₁ f₂
⊢ (∑ m ∈ Finset.antidiagonal (k₁ + k₂ - 1), (k₁ + k₂ - 1).choose m.1 • (f₁ ^ m.1 * f₂ ^ m.2)) (m₁ ⊗ₜ[R] m₂) = 0
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case mem.mem.inr.inr.inl
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
f x y u v : L
t : IsSl2Triple u v f
__spread✝⁻⁰ : Submodule R L := span R {v, f, u}
⊢ 2 • v ∈ span R {v, f, u}

Tactic:
]

Goal state after:
case mem.mem.inr.inr.inl
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
f x y u v : L
t : IsSl2Triple u v f
__spread✝⁻⁰ : Submodule R L := span R {v, f, u}
⊢ 2 • v ∈ span R {v, f, u}
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: 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
m : M
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
n : ℕ
IH : ((toEnd R L M) x ^ n) m ∈ genWeightSpace M (n • χ₁ + χ₂)
⊢ χ₁ + n • χ₁ + χ₂ = χ₁ + n • χ₁ + χ₂

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case mem.mem.inr.inr.inr.inl
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
e x y u v : L
t : IsSl2Triple u e v
__spread✝⁻⁰ : Submodule R L := span R {e, v, u}
⊢ 2 • v ∈ span R {e, v, u}

Tactic:
]

Goal state after:
case mem.mem.inr.inr.inr.inl
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
e x y u v : L
t : IsSl2Triple u e v
__spread✝⁻⁰ : Submodule R L := span R {e, v, u}
⊢ 2 • v ∈ span R {e, v, u}
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)
f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)
h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0
k₂ : ℕ
hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0
hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0
hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal (k₁ + k₂ - 1)
this : (f₁ ^ i * f₂ ^ j) (m₁ ⊗ₜ[R] m₂) = 0
⊢ (k₁ + k₂ - 1).choose (i, j).1 • 0 = 0

Tactic:
]

Goal state after:
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)
f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)
h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0
k₂ : ℕ
hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0
hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0
hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal (k₁ + k₂ - 1)
this : (f₁ ^ i * f₂ ^ j) (m₁ ⊗ₜ[R] m₂) = 0
⊢ (k₁ + k₂ - 1).choose (i, j).1 • 0 = 0
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case add
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
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : m ∈ ⨆ χ ∈ s, genWeightSpace M χ
x✝ y✝ : L
hx✝ : x✝ ∈ ⨆ i ∈ s, rootSpace H i
hy✝ : y✝ ∈ ⨆ i ∈ s, rootSpace H i
hu : ⁅x✝, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
hv : ⁅y✝, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
⊢ ⁅x✝, m⁆ + ⁅y✝, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

Tactic:
]

Goal state after:
case add
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
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : m ∈ ⨆ χ ∈ s, genWeightSpace M χ
x✝ y✝ : L
hx✝ : x✝ ∈ ⨆ i ∈ s, rootSpace H i
hy✝ : y✝ ∈ ⨆ i ∈ s, rootSpace H i
hu : ⁅x✝, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
hv : ⁅y✝, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
⊢ ⁅x✝, m⁆ + ⁅y✝, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
Module: Mathlib.Algebra.Lie.Weights.Cartan

Goal state before:
pp: case add
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
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : m ∈ ⨆ χ ∈ s, genWeightSpace M χ
x✝ y✝ : L
hx✝ : x✝ ∈ ⨆ i ∈ s, rootSpace H i
hy✝ : y✝ ∈ ⨆ i ∈ s, rootSpace H i
hu : ⁅x✝, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
hv : ⁅y✝, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ
⊢ ⁅x✝, m⁆ + ⁅y✝, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

Tactic:
exact add_mem hu hv

Goal state after: