awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor M₂
    (HSub.hSub (α := Module.End R M₁)
      (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x : Module.End R M₁)
      (HSMul.hSMul (β := Module.End R M₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
h_comm_square : F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ :
  Eq (α := M₁)
    ((HSub.hSub (α := Module.End R M₁)
              (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x :
                Module.End R M₁)
              (HSMul.hSMul (β := Module.End R M₁) χ₁ 1) ^
            k₁ :
          (a : M₁) → M₁)
        m₁ :
      M₁)
    (0 : M₁)
k₂ : ℕ
hk₂ :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) χ₂ 1) ^
            k₂ :
          (a : M₂) → M₂)
        m₂ :
      M₂)
    (0 : M₂)
hf₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ k₁ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf₂ : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ k₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (k₁ + k₂ - 1)
hi : k₁ ≤ (i, j).1
h : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ j * f₁ ^ i : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
h₁ :
  Eq (α := M₁ ⊗[R] M₂)
    ((f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) ((f₁ ^ i : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂)) : M₁ ⊗[R] M₂)
    (0 : M₁ ⊗[R] M₂)
h₂ : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) 0) 0
⊢ Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i * f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
have h₃ : Eq (α := M₁ ⊗[R] M₂) 0 0
Tactic: rw [(hf_comm.pow_pow i j).eq, Module.End.mul_apply, Module.End.pow_map_zero_of_le hi hf₁,
      map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor M₂
    (HSub.hSub (α := Module.End R M₁)
      (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x : Module.End R M₁)
      (HSMul.hSMul (β := Module.End R M₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
h_comm_square : F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ :
  Eq (α := M₁)
    ((HSub.hSub (α := Module.End R M₁)
              (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x :
                Module.End R M₁)
              (HSMul.hSMul (β := Module.End R M₁) χ₁ 1) ^
            k₁ :
          (a : M₁) → M₁)
        m₁ :
      M₁)
    (0 : M₁)
k₂ : ℕ
hk₂ :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) χ₂ 1) ^
            k₂ :
          (a : M₂) → M₂)
        m₂ :
      M₂)
    (0 : M₂)
hf₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ k₁ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf₂ : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ k₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (k₁ + k₂ - 1)
hj : k₂ ≤ (i, j).2
⊢ Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i * f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
have h : Eq (α := M₁ ⊗[R] M₂)
  ((f₁ ^ i : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) ((f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂)) : M₁ ⊗[R] M₂)
  (0 : M₁ ⊗[R] M₂)
Tactic: rw [Module.End.mul_apply, Module.End.pow_map_zero_of_le hj hf₂, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor M₂
    (HSub.hSub (α := Module.End R M₁)
      (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x : Module.End R M₁)
      (HSMul.hSMul (β := Module.End R M₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
h_comm_square : F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ :
  Eq (α := M₁)
    ((HSub.hSub (α := Module.End R M₁)
              (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x :
                Module.End R M₁)
              (HSMul.hSMul (β := Module.End R M₁) χ₁ 1) ^
            k₁ :
          (a : M₁) → M₁)
        m₁ :
      M₁)
    (0 : M₁)
k₂ : ℕ
hk₂ :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) χ₂ 1) ^
            k₂ :
          (a : M₂) → M₂)
        m₂ :
      M₂)
    (0 : M₂)
hf₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ k₁ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf₂ : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ k₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (k₁ + k₂ - 1)
hj : k₂ ≤ (i, j).2
h :
  Eq (α := M₁ ⊗[R] M₂)
    ((f₁ ^ i : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) ((f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂)) : M₁ ⊗[R] M₂)
    (0 : M₁ ⊗[R] M₂)
⊢ Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i * f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
have h₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) 0) 0
Tactic: rw [Module.End.mul_apply, Module.End.pow_map_zero_of_le hj hf₂, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁ : M₁
m₂ : M₂
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor M₂
    (HSub.hSub (α := Module.End R M₁)
      (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x : Module.End R M₁)
      (HSMul.hSMul (β := Module.End R M₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
h_comm_square : F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) = (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)
k₁ : ℕ
hk₁ :
  Eq (α := M₁)
    ((HSub.hSub (α := Module.End R M₁)
              (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x :
                Module.End R M₁)
              (HSMul.hSMul (β := Module.End R M₁) χ₁ 1) ^
            k₁ :
          (a : M₁) → M₁)
        m₁ :
      M₁)
    (0 : M₁)
k₂ : ℕ
hk₂ :
  Eq (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) χ₂ 1) ^
            k₂ :
          (a : M₂) → M₂)
        m₂ :
      M₂)
    (0 : M₂)
hf₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ k₁ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf₂ : Eq (α := M₁ ⊗[R] M₂) ((f₂ ^ k₂ : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
hf_comm : Commute f₁ f₂
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ (k₁ + k₂ - 1)
hj : k₂ ≤ (i, j).2
h :
  Eq (α := M₁ ⊗[R] M₂)
    ((f₁ ^ i : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) ((f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂)) : M₁ ⊗[R] M₂)
    (0 : M₁ ⊗[R] M₂)
h₁ : Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) 0) 0
⊢ Eq (α := M₁ ⊗[R] M₂) ((f₁ ^ i * f₂ ^ j : (a : M₁ ⊗[R] M₂) → M₁ ⊗[R] M₂) (m₁ ⊗ₜ[R] m₂) : M₁ ⊗[R] M₂) (0 : M₁ ⊗[R] M₂)
have h₂ : Eq (α := M₁ ⊗[R] M₂) 0 0
Tactic: rw [Module.End.mul_apply, Module.End.pow_map_zero_of_le hj hf₂, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
χ₁ χ₂ : R
x y : L
m : M
hy : Membership.mem (γ := Submodule R L) 𝕎(L, χ₁, x) y
hm : Membership.mem (γ := Submodule R M) 𝕎(M, χ₂, x) m
⊢ Membership.mem (γ := Submodule R M) 𝕎(M, χ₁ + χ₂, x) ⁅y, m⁆
have a : Membership.mem (γ := Submodule R M)
  (LinearMap.range (M := TensorProduct.{u_2, u_3, u_4} R ↥𝕎(L, χ₁, x) ↥𝕎(M, χ₂, x))
    ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) ∘ₗ TensorProduct.mapIncl 𝕎(L, χ₁, x) 𝕎(M, χ₂, x)))
  ⁅y, m⁆
Tactic: apply LieModule.weight_vector_multiplication L M M (toModuleHom R L M) χ₁ χ₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
χ₁ χ₂ : R
x y : L
m : M
hy : Membership.mem (γ := Submodule R L) 𝕎(L, χ₁, x) y
hm : Membership.mem (γ := Submodule R M) 𝕎(M, χ₂, x) m
⊢ Membership.mem (γ := Submodule R M)
    (LinearMap.range (M := TensorProduct.{u_2, u_3, u_4} R ↥𝕎(L, χ₁, x) ↥𝕎(M, χ₂, x))
      ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) ∘ₗ TensorProduct.mapIncl 𝕎(L, χ₁, x) 𝕎(M, χ₂, x)))
    ⁅y, m⁆
have a : ∃ (y_1 : TensorProduct.{u_2, u_3, u_4} R ↥𝕎(L, χ₁, x) ↥𝕎(M, χ₂, x)),
  (toModuleHom R L M : (a : L ⊗[R] M) → M)
      ((TensorProduct.map (Submodule.subtype 𝕎(L, χ₁, x)) (Submodule.subtype 𝕎(M, χ₂, x)) :
            (a : ↥𝕎(L, χ₁, x) ⊗[R] ↥𝕎(M, χ₂, x)) → L ⊗[R] M)
          y_1 :
        L ⊗[R] M) =
    ⁅y, m⁆
Tactic: simp only [LieModuleHom.coe_toLinearMap, Function.comp_apply, LinearMap.coe_comp,
    TensorProduct.mapIncl, LinearMap.mem_range]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
χ₁ χ₂ : R
x y : L
m : M
hy : Membership.mem (γ := Submodule R L) 𝕎(L, χ₁, x) y
hm : Membership.mem (γ := Submodule R M) 𝕎(M, χ₂, x) m
⊢ ∃ (y_1 : TensorProduct.{u_2, u_3, u_4} R ↥𝕎(L, χ₁, x) ↥𝕎(M, χ₂, x)),
    (toModuleHom R L M : (a : L ⊗[R] M) → M)
        ((TensorProduct.map (Submodule.subtype 𝕎(L, χ₁, x)) (Submodule.subtype 𝕎(M, χ₂, x)) :
              (a : ↥𝕎(L, χ₁, x) ⊗[R] ↥𝕎(M, χ₂, x)) → L ⊗[R] M)
            y_1 :
          L ⊗[R] M) =
      ⁅y, m⁆
have h : (toModuleHom R L M : (a : L ⊗[R] M) → M)
    ((TensorProduct.map (Submodule.subtype 𝕎(L, χ₁, x)) (Submodule.subtype 𝕎(M, χ₂, x)) :
          (a : ↥𝕎(L, χ₁, x) ⊗[R] ↥𝕎(M, χ₂, x)) → L ⊗[R] M)
        (Subtype.mk (p := fun (x_1 : L) ↦ Membership.mem (γ := Submodule R L) 𝕎(L, χ₁, x) x_1) y hy ⊗ₜ[R]
          Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submodule R M) 𝕎(M, χ₂, x) x_1) m hm) :
      L ⊗[R] M) =
  ⁅y, m⁆
Tactic: use ⟨y, hy⟩ ⊗ₜ ⟨m, hm⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : R
x y : L
m : M
hm :
  Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid 𝕎(M, χ, x)))) m
⊢ Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid 𝕎(M, χ, x)))) ⁅y, m⁆
have hm₁ : Membership.mem (γ := Submodule R M) 𝕎(M, χ, x) m
Tactic: simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
        Submodule.mem_toAddSubmonoid] at hm ⊢
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : R
x y : L
m : M
hm : Membership.mem (γ := Submodule R M) 𝕎(M, χ, x) m
⊢ Membership.mem (γ := Submodule R M) 𝕎(M, χ, x) ⁅y, m⁆
have rw : Membership.mem (γ := Submodule R M) 𝕎(M, 0 + χ, x) ⁅y, m⁆
Tactic: rw [← zero_add χ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
⊢ LE.le (α := LieSubmodule R L M) (weightSpace M χ) (genWeightSpace M χ)
have h : ∀ (i : L), LE.le (α := LieSubmodule R L M) (weightSpace M χ) (genWeightSpaceOf M (χ i) i)
Tactic: apply le_iInf
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
x : L
⊢ LE.le (α := Submodule R M)
    ((LieSubmodule.toSubmodule_orderEmbedding R L M : (a : LieSubmodule R L M) → Submodule R M) (weightSpace M χ) :
      Submodule R M)
    ((LieSubmodule.toSubmodule_orderEmbedding R L M : (a : LieSubmodule R L M) → Submodule R M)
        (genWeightSpaceOf M (χ x) x) :
      Submodule R M)
have h : LE.le.{u_4} (α := Submodule R M)
  (Module.End.eigenspace (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x)
    (χ x))
  ((LieSubmodule.toSubmodule_orderEmbedding R L M : (a : LieSubmodule R L M) → Submodule R M)
    (genWeightSpaceOf M (χ x) x))
Tactic: apply (iInf_le _ x).trans
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ₁ χ₂ : Weight R L M
h : Eq (α := (a : L) → R) ((fun (χ : Weight R L M) ↦ χ.toFun) χ₁) ((fun (χ : Weight R L M) ↦ χ.toFun) χ₂)
⊢ χ₁ = χ₂
have mk : ∀ (toFun : L → R) (genWeightSpace_ne_bot' : Ne (α := LieSubmodule R L M) (genWeightSpace M toFun) ⊥)
  (h :
    Eq (α := (a : L) → R)
      ((fun (χ : Weight R L M) ↦ χ.toFun) { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' })
      ((fun (χ : Weight R L M) ↦ χ.toFun) χ₂)),
  { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' : Weight R L M } = χ₂
Tactic: cases χ₁
Cleared hypotheses: χ₁, h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
K : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ₂ : Weight R L M
toFun : L → R
genWeightSpace_ne_bot' : Ne (α := LieSubmodule R L M) (genWeightSpace M toFun) ⊥
h :
  Eq (α := (a : L) → R)
    ((fun (χ : Weight R L M) ↦ χ.toFun) { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' })
    ((fun (χ : Weight R L M) ↦ χ.toFun) χ₂)
⊢ { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' : Weight R L M } = χ₂
have mk : ∀ (toFun_1 : L → R) (genWeightSpace_ne_bot'_1 : Ne (α := LieSubmodule R L M) (genWeightSpace M toFun_1) ⊥)
  (h :
    Eq (α := (a : L) → R)
      ((fun (χ : Weight R L M) ↦ χ.toFun) { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' })
      ((fun (χ : Weight R L M) ↦ χ.toFun) { toFun := toFun_1, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'_1 })),
  { toFun := toFun, genWeightSpace_ne_bot' := genWeightSpace_ne_bot' : Weight R L M } =
    { toFun := toFun_1, genWeightSpace_ne_bot' := genWeightSpace_ne_bot'_1 }
Tactic: cases χ₂
Cleared hypotheses: χ₂, h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : Weight R L M
x : L
⊢ Ne (α := LieSubmodule R L M) (genWeightSpaceOf M ((χ : (a : L) → R) x) x : LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)
have this : Ne.{u_4 + 1} (α := LieSubmodule R L M) (⨅ (x : L), genWeightSpaceOf M ((χ : (a : L) → R) x) x) ⊥
Tactic: have : ⨅ x, genWeightSpaceOf M (χ x) x ≠ ⊥ := χ.genWeightSpace_ne_bot
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : Weight R L M
x : L
this : Ne.{u_4 + 1} (α := LieSubmodule R L M) (⨅ (x : L), genWeightSpaceOf M ((χ : (a : L) → R) x) x) ⊥
⊢ Ne (α := LieSubmodule R L M) (genWeightSpaceOf M ((χ : (a : L) → R) x) x : LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)
have contrapose : ∀
  (this :
    Eq (α := LieSubmodule R L M) (genWeightSpaceOf M ((χ : (a : L) → R) x) x : LieSubmodule R L M)
      (⊥ : LieSubmodule R L M)),
  Eq.{u_4 + 1} (α := LieSubmodule R L M) (⨅ (x : L), genWeightSpaceOf M ((χ : (a : L) → R) x) x) ⊥
Tactic: contrapose this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : Weight R L M
x : L
this :
  Eq (α := LieSubmodule R L M) (genWeightSpaceOf M ((χ : (a : L) → R) x) x : LieSubmodule R L M)
    (⊥ : LieSubmodule R L M)
⊢ Eq.{u_4 + 1} (α := LieSubmodule R L M) (⨅ (x : L), genWeightSpaceOf M ((χ : (a : L) → R) x) x) ⊥
have rw : LE.le.{u_4} (α := LieSubmodule R L M) (⨅ (x : L), genWeightSpaceOf M ((χ : (a : L) → R) x) x) ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : Weight R L M
x : L
⊢ Module.End.HasEigenvalue.{u_2, u_4} (R := R) (M := M)
    (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    ((χ : (a : L) → R) x : R)
have obtain : ∀ (k : ℕ)
  (hk :
    Ne.{u_4 + 1} (α := Submodule R M)
      (((Module.End.genEigenspace
                (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x)
                ((χ : (a : L) → R) x) :
              ℕ∞ →o Submodule R M) :
            (a : ℕ∞) → Submodule R M)
          (↑k : ℕ∞) :
        Submodule R M)
      (⊥ : Submodule R M)),
  Module.End.HasEigenvalue.{u_2, u_4} (R := R) (M := M)
    (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    ((χ : (a : L) → R) x : R)
Tactic: obtain ⟨k : ℕ, hk : (toEnd R L M x).genEigenspace (χ x) k ≠ ⊥⟩ := by
    simpa [genWeightSpaceOf, ← Module.End.iSup_genEigenspace_eq] using χ.genWeightSpaceOf_ne_bot x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : LieRing.IsNilpotent L
χ : L → R
⊢ Eq (α := Submodule R M) (↑(genWeightSpace M (χ ∘ (⇑(LieSubalgebra.incl ⊤) : (a : ↥⊤) → L))) : Submodule R M)
    (↑(genWeightSpace M χ) : Submodule R M)
have h : ∀ (m : M),
  Membership.mem (γ := Submodule R M)
      (↑(genWeightSpace M (χ ∘ (⇑(LieSubalgebra.incl ⊤) : (a : ↥⊤) → L))) : Submodule R M) m ↔
    Membership.mem (γ := Submodule R M) (↑(genWeightSpace M χ) : Submodule R M) m
Tactic: ext m