awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H α
y : M
hy :
  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
    (⨆ (x : Subtype (Membership.mem (Ioo p q))), genWeightSpace M ((↑x : ℤ) • α + χ)) y
mem :
  ∀ (k : Subtype (Membership.mem (Ioo p q))) (z : M)
    (hz : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M ((↑k : ℤ) • α + χ)) z),
    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, z⁆
zero : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, 0⁆
add :
  ∀ (x_1 y : M),
    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
        (⨆ (i : Subtype (Membership.mem (Ioo p q))), genWeightSpace M ((↑i : ℤ) • α + χ)) x_1 →
      Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M)
          (⨆ (i : Subtype (Membership.mem (Ioo p q))), genWeightSpace M ((↑i : ℤ) • α + χ)) y →
        ∀ (hz₁ : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, x_1⁆)
          (hz₂ : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, y⁆),
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, x_1 + y⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, y⁆

Tactic:
induction hy using LieSubmodule.iSup_induction' with
  | mem k z hz =>
    obtain ⟨k, hk⟩ := k
    suffices genWeightSpace M ((k + 1) • α + χ) ≤ genWeightSpaceChain M α χ p q by
      apply this
      -- was `simpa using [...]` and very slow
      -- (https://github.com/leanprover-community/mathlib4/issues/19751)
      simpa only [zsmul_eq_mul, Int.cast_add, Pi.intCast_def, Int.cast_one] using
        (rootSpaceWeightSpaceProduct R L H M α (k • α + χ) ((k + 1) • α + χ)
            (by rw [add_smul]; abel) (⟨x, hx⟩ ⊗ₜ ⟨z, hz⟩)).property
    rw [genWeightSpaceChain]
    rcases eq_or_ne (k + 1) q with rfl | hk'; · simp only [hq, bot_le]
    replace hk' : k + 1 ∈ Ioo p q := ⟨by linarith [hk.1], lt_of_le_of_ne hk.2 hk'⟩
    exact le_biSup (fun k ↦ genWeightSpace M (k • α + χ)) hk'
  | zero => simp
  | add _ _ _ _ hz₁ hz₂ => rw [lie_add]; exact add_mem hz₁ hz₂

Premises used: LieModule.genWeightSpaceChain, bot_le, rfl, lie_add
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) y
rwa : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (-(-p • α) + χ)) ⊥
rwa₁ : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (- -(p • α) + χ)) ⊥
rwa₂ rwa₃ rwa₄ rwa₅ : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
⊢ Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (-p • -α + χ)) ⊥

Tactic:
rwa [smul_neg, neg_smul, neg_neg]

Premises used: neg_smul, neg_neg, smul_neg
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) y
⊢ Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (-p • -α + χ)) ⊥

Tactic:
replace hp : genWeightSpace M ((-p) • (-α) + χ) = ⊥ := by rwa [smul_neg, neg_smul, neg_neg]
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) y
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (-p • -α + χ)) ⊥
rw :
  ∀ (hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M (-α) χ (-q) (-p)) y)
    (hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (-p • -α + χ)) ⊥),
    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M (-α) χ (-q) (-p)) ⁅x, y⁆
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) ⁅x, y⁆

Tactic:
rw [← genWeightSpaceChain_neg] at hy ⊢

Premises used: LieModule.genWeightSpaceChain_neg
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M (-α) χ (-q) (-p)) y
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (-p • -α + χ)) ⊥
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M (-α) χ (-q) (-p)) ⁅x, y⁆

Tactic:
lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right M (-α) χ (-q) (-p) hp hx hy

Premises used: LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right, Neg.neg
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : LieRing.IsNilpotent.{u_2} ↥H
x : L
hx : x ∈ rootSpace H (-α)
y : M
hy : Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M (-α) χ (-q) (-p)) y
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (-p • -α + χ)) ⊥
⊢ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M (-α) χ (-q) (-p)) ⁅x, y⁆

Tactic:
exact lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right M (-α) χ (-q) (-p) hp hx hy

Premises used: LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right, Neg.neg
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : ↥H
hx : x ∈ corootSpace α
⊢ Membership.mem (γ := Submodule R ↥H)
    (Submodule.span R {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}) x

Tactic:
rw [LieAlgebra.mem_corootSpace'] at hx

Premises used: LieAlgebra.mem_corootSpace'
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x u : ↥H
hu : Membership.mem (γ := Set ↥H) {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)} u
mem :
  ∀ (y : L) (hy : y ∈ rootSpace H α) (z : L) (hz : z ∈ rootSpace H (-α)) (hyz : ⁅y, z⁆ = (↑u : L)),
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
            (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
          (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
                  LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
                (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
              u :
            End R ↥(genWeightSpaceChain M α χ p q)) :
        R)
      (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
          (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
        (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
                LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
              (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
            u :
          End R ↥(genWeightSpaceChain M α χ p q)) :
      R)
    (0 : R)

Tactic:
obtain ⟨y, hy, z, hz, hyz⟩ := hu
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = (↑u : L)
x_1 x_2 : ↥(genWeightSpaceChain M α χ p q)
⊢ (match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x_1 + x_2 with
    | ⟨m, hm⟩ =>
      Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅y, m⁆ ⋯) =
    HAdd.hAdd (α := ↥(genWeightSpaceChain M α χ p q)) (β := ↥(genWeightSpaceChain M α χ p q))
      (match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x_1 with
        | ⟨m, hm⟩ =>
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅y, m⁆ ⋯ :
        ↥(genWeightSpaceChain M α χ p q))
      (match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x_2 with
        | ⟨m, hm⟩ =>
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅y, m⁆ ⋯ :
        ↥(genWeightSpaceChain M α χ p q))

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = (↑u : L)
t : R
m : ↥(genWeightSpaceChain M α χ p q)
⊢ (match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) t • m with
    | ⟨m, hm⟩ =>
      Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅y, m⁆ ⋯) =
    HSMul.hSMul (α := R) (β := ↥(genWeightSpaceChain M α χ p q)) ((RingHom.id R : (a : R) → R) t : R)
      (match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) m with
        | ⟨m, hm⟩ =>
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅y, m⁆ ⋯ :
        ↥(genWeightSpaceChain M α χ p q))

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = (↑u : L)
f : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun (x : ↥(genWeightSpaceChain M α χ p q)) ↦
      match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x with
      | ⟨m, hm⟩ =>
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅y, m⁆ ⋯,
    map_add' := ⋯, map_smul' := ⋯ }
x_1 x_2 : ↥(genWeightSpaceChain M α χ p q)
⊢ (match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x_1 + x_2 with
    | ⟨m, hm⟩ =>
      Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅z, m⁆ ⋯) =
    HAdd.hAdd (α := ↥(genWeightSpaceChain M α χ p q)) (β := ↥(genWeightSpaceChain M α χ p q))
      (match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x_1 with
        | ⟨m, hm⟩ =>
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅z, m⁆ ⋯ :
        ↥(genWeightSpaceChain M α χ p q))
      (match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x_2 with
        | ⟨m, hm⟩ =>
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅z, m⁆ ⋯ :
        ↥(genWeightSpaceChain M α χ p q))

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = (↑u : L)
f : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun (x : ↥(genWeightSpaceChain M α χ p q)) ↦
      match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x with
      | ⟨m, hm⟩ =>
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅y, m⁆ ⋯,
    map_add' := ⋯, map_smul' := ⋯ }
t : R
m : ↥(genWeightSpaceChain M α χ p q)
⊢ (match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) t • m with
    | ⟨m, hm⟩ =>
      Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅z, m⁆ ⋯) =
    HSMul.hSMul (α := R) (β := ↥(genWeightSpaceChain M α χ p q)) ((RingHom.id R : (a : R) → R) t : R)
      (match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) m with
        | ⟨m, hm⟩ =>
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅z, m⁆ ⋯ :
        ↥(genWeightSpaceChain M α χ p q))

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = (↑u : L)
f : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun (x : ↥(genWeightSpaceChain M α χ p q)) ↦
      match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x with
      | ⟨m, hm⟩ =>
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅y, m⁆ ⋯,
    map_add' := ⋯, map_smul' := ⋯ }
g : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun (x : ↥(genWeightSpaceChain M α χ p q)) ↦
      match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x with
      | ⟨m, hm⟩ =>
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅z, m⁆ ⋯,
    map_add' := ⋯, map_smul' := ⋯ }
h :
  ∀ (x : ↥(genWeightSpaceChain M α χ p q)),
    Eq.{u_3 + 1} (α := M)
      (↑(((((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
                      LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
                    (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
                  u :
                End R ↥(genWeightSpaceChain M α χ p q)) :
              (a : ↥(genWeightSpaceChain M α χ p q)) → ↥(genWeightSpaceChain M α χ p q))
            x) :
        M)
      (↑((⁅f, g⁆ : (a : ↥(genWeightSpaceChain M α χ p q)) → ↥(genWeightSpaceChain M α χ p q)) x) : M)
⊢ ((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
          LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
        (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
      u =
    ⁅f, g⁆

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = (↑u : L)
f : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun (x : ↥(genWeightSpaceChain M α χ p q)) ↦
      match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x with
      | ⟨m, hm⟩ =>
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅y, m⁆ ⋯,
    map_add' := ⋯, map_smul' := ⋯ }
g : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun (x : ↥(genWeightSpaceChain M α χ p q)) ↦
      match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x with
      | ⟨m, hm⟩ =>
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅z, m⁆ ⋯,
    map_add' := ⋯, map_smul' := ⋯ }
x_1 : ↥(genWeightSpaceChain M α χ p q)
h :
  ⁅⁅y, z⁆, (↑x_1 : M)⁆ =
    (↑((⁅f, g⁆ : (a : ↥(genWeightSpaceChain M α χ p q)) → ↥(genWeightSpaceChain M α χ p q)) x_1) : M)
⊢ Eq.{u_3 + 1} (α := M)
    (↑(((((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
                    LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
                  (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
                u :
              End R ↥(genWeightSpaceChain M α χ p q)) :
            (a : ↥(genWeightSpaceChain M α χ p q)) → ↥(genWeightSpaceChain M α χ p q))
          x_1) :
      M)
    (↑((⁅f, g⁆ : (a : ↥(genWeightSpaceChain M α χ p q)) → ↥(genWeightSpaceChain M α χ p q)) x_1) : M)

Tactic:
rw [toEnd_apply_apply, LieSubmodule.coe_bracket, LieSubalgebra.coe_bracket_of_module, ← hyz]

Premises used: LieSubalgebra.coe_bracket_of_module, LieModule.toEnd_apply_apply, LieSubmodule.coe_bracket
-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = (↑u : L)
f : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun (x : ↥(genWeightSpaceChain M α χ p q)) ↦
      match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x with
      | ⟨m, hm⟩ =>
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅y, m⁆ ⋯,
    map_add' := ⋯, map_smul' := ⋯ }
g : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun (x : ↥(genWeightSpaceChain M α χ p q)) ↦
      match (motive := ↥(genWeightSpaceChain M α χ p q) → ↥(genWeightSpaceChain M α χ p q)) x with
      | ⟨m, hm⟩ =>
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpaceChain M α χ p q) x) ⁅z, m⁆ ⋯,
    map_add' := ⋯, map_smul' := ⋯ }
x_1 : ↥(genWeightSpaceChain M α χ p q)
⊢ ⁅⁅y, z⁆, (↑x_1 : M)⁆ =
    (↑((⁅f, g⁆ : (a : ↥(genWeightSpaceChain M α χ p q)) → ↥(genWeightSpaceChain M α χ p q)) x_1) : M)

Tactic:
simp only [lie_lie, LieHom.lie_apply, LinearMap.coe_mk, AddHom.coe_mk, Module.End.lie_apply,
        AddSubgroupClass.coe_sub, f, g]

Premises used: AddSubgroupClass.coe_sub, LinearMap.coe_mk, LieHom.lie_apply, Module.End.lie_apply, AddHom.coe_mk, lie_lie