awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) (⁅x_1, m⁆ + ⁅y, m⁆)

Tactic:
add_mem hu hv

Premises used: AddMemClass.add_mem
-- 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⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) (⁅x_1, m⁆ + ⁅y, m⁆)

Tactic:
exact add_mem hu hv

Premises used: AddMemClass.add_mem
-- 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
χ₁ : ↥H → R
u : L
hu : Membership.mem (γ := LieSubmodule R (↥H) L) (⨆ (_ : χ₁ ∈ s), rootSpace H χ₁) u
pos : ∀ (hχ₁ : χ₁ ∈ s), Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, m⁆
neg : ∀ (hχ₁ : χ₁ ∉ s), Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, m⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, m⁆

Tactic:
by_cases hχ₁ : χ₁ ∈ s
-- 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
χ₁ : ↥H → R
u : L
hu : Membership.mem (γ := LieSubmodule R (↥H) L) (⨆ (_ : χ₁ ∈ s), rootSpace H χ₁) u
hχ₁ : χ₁ ∉ s
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, m⁆

Tactic:
simp_all
-- 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
χ₁ : ↥H → R
u : L
hu : Membership.mem (γ := LieSubmodule R (↥H) L) (⨆ (_ : χ₁ ∈ s), rootSpace H χ₁) u
hχ₁ : χ₁ ∈ s
⊢ u ∈ rootSpace H χ₁

Tactic:
simpa [hχ₁] using hu
-- 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
χ₁ : ↥H → R
u : L
hu : Membership.mem (γ := LieSubmodule R (↥H) L) (⨆ (_ : χ₁ ∈ s), rootSpace H χ₁) u
hχ₁ : χ₁ ∈ s
⊢ u ∈ rootSpace H χ₁

Tactic:
replace hu : u ∈ rootSpace H χ₁ := by simpa [hχ₁] using hu
-- 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
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, 0⁆

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
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
x_1 y : M
hx : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ i ∈ s, genWeightSpace M i) x_1
hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ i ∈ s, genWeightSpace M i) y
hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, x_1⁆
hw : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, y⁆
pos : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) (⁅u, x_1⁆ + ⁅u, y⁆)
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, x_1 + y⁆

Tactic:
rw [lie_add]

Premises used: lie_add
-- 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
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
x_1 y : M
hx : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ i ∈ s, genWeightSpace M i) x_1
hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ i ∈ s, genWeightSpace M i) y
hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, x_1⁆
hw : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, y⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) (⁅u, x_1⁆ + ⁅u, y⁆)

Tactic:
add_mem hv hw

Premises used: AddMemClass.add_mem
-- 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
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
x_1 y : M
hx : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ i ∈ s, genWeightSpace M i) x_1
hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ i ∈ s, genWeightSpace M i) y
hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, x_1⁆
hw : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, y⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) (⁅u, x_1⁆ + ⁅u, y⁆)

Tactic:
exact add_mem hv hw

Premises used: AddMemClass.add_mem
-- 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
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
χ₂ : ↥H → R
v : M
hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ (_ : χ₂ ∈ s), genWeightSpace M χ₂) v
pos : ∀ (hχ₂ : χ₂ ∈ s), Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, v⁆
neg : ∀ (hχ₂ : χ₂ ∉ s), Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, v⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, v⁆

Tactic:
by_cases hχ₂ : χ₂ ∈ s
-- 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
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
χ₂ : ↥H → R
v : M
hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ (_ : χ₂ ∈ s), genWeightSpace M χ₂) v
hχ₂ : χ₂ ∉ s
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, v⁆

Tactic:
simp_all
-- 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
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
χ₂ : ↥H → R
v : M
hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ (_ : χ₂ ∈ s), genWeightSpace M χ₂) v
hχ₂ : χ₂ ∈ s
pos :
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ (_ : χ₁ + χ₂ ∈ s), genWeightSpace M (χ₁ + χ₂)) ⁅u, v⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, v⁆

Tactic:
apply LieSubmodule.mem_iSup_of_mem (χ₁ + χ₂)

Premises used: LieSubmodule.mem_iSup_of_mem, HAdd.hAdd
-- 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
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
χ₂ : ↥H → R
v : M
hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ (_ : χ₂ ∈ s), genWeightSpace M χ₂) v
hχ₂ : χ₂ ∈ s
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ (_ : χ₁ + χ₂ ∈ s), genWeightSpace M (χ₁ + χ₂)) ⁅u, v⁆

Tactic:
simp_all [lie_mem_genWeightSpace_of_mem_genWeightSpace]

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
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
χ₁ : ↥H → R
u : L
hχ₁ : χ₁ ∈ s
hu : u ∈ rootSpace H χ₁
pos : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, 0⁆
pos₁ :
  ∀ (x y : M),
    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ i ∈ s, genWeightSpace M i) x →
      Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ i ∈ s, genWeightSpace M i) y →
        ∀ (hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, x⁆)
          (hw : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, y⁆),
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, x + y⁆
pos₂ :
  ∀ (χ₂ : ↥H → R) (v : M)
    (hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ (_ : χ₂ ∈ s), genWeightSpace M χ₂) v),
    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, v⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, m⁆

Tactic:
induction hm using LieSubmodule.iSup_induction' with
    | zero => simp
    | add _ _ _ _ hv hw => rw [lie_add]; exact add_mem hv hw
    | mem χ₂ v hv =>
      by_cases hχ₂ : χ₂ ∈ s; swap
      · simp_all
      apply LieSubmodule.mem_iSup_of_mem (χ₁ + χ₂)
      simp_all [lie_mem_genWeightSpace_of_mem_genWeightSpace]

Premises used: LieAlgebra.lie_mem_genWeightSpace_of_mem_genWeightSpace, lie_add
-- 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
hx : Membership.mem (γ := LieSubmodule R (↥H) L) (⨆ χ ∈ s, rootSpace H χ) x
hm : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) m
zero :
  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)
add :
  ∀ (x y : L),
    Membership.mem (γ := LieSubmodule R (↥H) L) (⨆ i ∈ s, rootSpace H i) x →
      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, m⁆)
          (hv : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅y, m⁆),
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅x + y, m⁆
mem :
  ∀ (χ₁ : ↥H → R) (u : L) (hu : Membership.mem (γ := LieSubmodule R (↥H) L) (⨆ (_ : χ₁ ∈ s), rootSpace H χ₁) u),
    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅u, m⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (⨆ χ ∈ s, genWeightSpace M χ) ⁅x, m⁆

Tactic:
induction hx using LieSubmodule.iSup_induction' with
  | zero => simp
  | add _ _ _ _ hu hv => rw [add_lie]; exact add_mem hu hv
  | mem χ₁ u hu =>
    by_cases hχ₁ : χ₁ ∈ s; swap
    · simp_all
    replace hu : u ∈ rootSpace H χ₁ := by simpa [hχ₁] using hu
    induction hm using LieSubmodule.iSup_induction' with
    | zero => simp
    | add _ _ _ _ hv hw => rw [lie_add]; exact add_mem hv hw
    | mem χ₂ v hv =>
      by_cases hχ₂ : χ₂ ∈ s; swap
      · simp_all
      apply LieSubmodule.mem_iSup_of_mem (χ₁ + χ₂)
      simp_all [lie_mem_genWeightSpace_of_mem_genWeightSpace]

Premises used: LieAlgebra.lie_mem_genWeightSpace_of_mem_genWeightSpace, lie_add, add_lie
-- 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
hχ : χ₁ + χ₂ = χ₃
x : ↥(rootSpace H χ₁)
m n : ↥(genWeightSpace M χ₂)
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
      ⁅(↑x : L), (↑(m + n) : M)⁆ ⋯ =
    HAdd.hAdd (α := ↥(genWeightSpace M χ₃))
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x) ⁅(↑x : L), (↑m : M)⁆ ⋯)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x) ⁅(↑x : L), (↑n : M)⁆ ⋯)

Tactic:
simp only [LieSubmodule.coe_add, lie_add, AddMemClass.mk_add_mk]

Premises used: AddMemClass.mk_add_mk, LieSubmodule.coe_add, lie_add
-- 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
hχ : χ₁ + χ₂ = χ₃
x : ↥(rootSpace H χ₁)
t : R
m : ↥(genWeightSpace M χ₂)
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
      ⁅(↑x : L), (↑(t • m) : M)⁆ ⋯ =
    HSMul.hSMul (α := R) (β := ↥(genWeightSpace M χ₃)) ((RingHom.id R : (a : R) → R) t : R)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x) ⁅(↑x : L), (↑m : 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
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
x y : ↥(rootSpace H χ₁)
h :
  ∀ (m : ↥(genWeightSpace M χ₂)),
    Eq.{u_3 + 1} (α := M)
      (↑(({
                toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
                  Subtype.mk (p := fun (x : M) ↦
                    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
                    ⁅(↑(x + y) : L), (↑m : M)⁆ ⋯,
                map_add' := ⋯, map_smul' := ⋯ } :
              (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
            m) :
        M)
      (↑((HAdd.hAdd (α := ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃))
                {
                  toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
                    Subtype.mk (p := fun (x : M) ↦
                      Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
                      ⁅(↑x : L), (↑m : M)⁆ ⋯,
                  map_add' := ⋯, map_smul' := ⋯ : ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃) }
                {
                  toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
                    Subtype.mk (p := fun (x : M) ↦
                      Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
                      ⁅(↑y : L), (↑m : M)⁆ ⋯,
                  map_add' := ⋯, map_smul' := ⋯ : ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃) } :
              (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
            m) :
        M)
⊢ {
      toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
          ⁅(↑(x + y) : L), (↑m : M)⁆ ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃))
      {
        toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x) ⁅(↑x : L), (↑m : M)⁆ ⋯,
        map_add' := ⋯, map_smul' := ⋯ : ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃) }
      {
        toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x) ⁅(↑y : L), (↑m : M)⁆ ⋯,
        map_add' := ⋯, map_smul' := ⋯ : ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃) }

Tactic:
ext m
-- 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
hχ : χ₁ + χ₂ = χ₃
x y : ↥(rootSpace H χ₁)
m : ↥(genWeightSpace M χ₂)
⊢ Eq.{u_3 + 1} (α := M)
    (↑(({
              toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
                Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
                  ⁅(↑(x + y) : L), (↑m : M)⁆ ⋯,
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
          m) :
      M)
    (↑((HAdd.hAdd (α := ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃))
              {
                toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
                  Subtype.mk (p := fun (x : M) ↦
                    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
                    ⁅(↑x : L), (↑m : M)⁆ ⋯,
                map_add' := ⋯, map_smul' := ⋯ : ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃) }
              {
                toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
                  Subtype.mk (p := fun (x : M) ↦
                    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
                    ⁅(↑y : L), (↑m : M)⁆ ⋯,
                map_add' := ⋯, map_smul' := ⋯ : ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃) } :
            (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
          m) :
      M)

Tactic:
simp only [LieSubmodule.coe_add, add_lie, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply,
      AddMemClass.mk_add_mk]

Premises used: LinearMap.coe_mk, LinearMap.add_apply, AddMemClass.mk_add_mk, AddHom.coe_mk, LieSubmodule.coe_add, add_lie