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 : H.IsCartanSubalgebra
inst_4 : IsNoetherian R L
rw : (↑(rootSpace H 0) : Submodule R L) = (↑H.toLieSubmodule : Submodule R L)
rw₁ : (zeroRootSubalgebra R L H).toSubmodule = (↑H.toLieSubmodule : Submodule R L)
rw₂ : H.toSubmodule = (↑H.toLieSubmodule : Submodule R L)
rw₃ rw₄ : H.toSubmodule = H.toSubmodule
⊢ rootSpace H 0 = H.toLieSubmodule

Tactic:
rw [← LieSubmodule.toSubmodule_inj, ← coe_zeroRootSubalgebra,
    zeroRootSubalgebra_eq_of_is_cartan R L H, LieSubalgebra.coe_toLieSubmodule]

Premises used: LieAlgebra.coe_zeroRootSubalgebra, LieSubmodule.toSubmodule_inj, LieAlgebra.zeroRootSubalgebra_eq_of_is_cartan, LieSubalgebra.coe_toLieSubmodule
-- 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
inst_8 : H.IsCartanSubalgebra
inst_9 : IsNoetherian R L
α : ↥H → R
rw :
  ∀ (m : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))),
    Membership.mem (α := L) (rootSpace H 0)
      (((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯) :
            (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → L)
          m :
        L)
⊢ ∀ (m : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))),
    Membership.mem (α := L) H.toLieSubmodule
      (((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯) :
            (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → L)
          m :
        L)

Tactic:
rw [← rootSpace_zero_eq]

Premises used: LieAlgebra.rootSpace_zero_eq
-- 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
inst_8 : H.IsCartanSubalgebra
inst_9 : IsNoetherian R L
α : ↥H → R
⊢ ∀ (m : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))),
    Membership.mem (α := L) (rootSpace H 0)
      (((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯) :
            (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → L)
          m :
        L)

Tactic:
fun p ↦ (rootSpaceProduct R L H α (-α) 0 (add_neg_cancel α) p).property

Premises used: add_neg_cancel, Set.Mem, setOf, LieAlgebra.rootSpaceProduct, OfNat.ofNat, DFunLike.coe, Neg.neg, Subtype.property
-- 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
inst_8 : H.IsCartanSubalgebra
inst_9 : IsNoetherian R L
α : ↥H → R
⊢ ∀ (m : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))),
    Membership.mem (α := L) (rootSpace H 0)
      (((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯) :
            (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → L)
          m :
        L)

Tactic:
exact fun p ↦ (rootSpaceProduct R L H α (-α) 0 (add_neg_cancel α) p).property

Premises used: add_neg_cancel, LieAlgebra.rootSpaceProduct, OfNat.ofNat, DFunLike.coe, Neg.neg, Subtype.property
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
simp :
  (∃ (m : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))),
      ((LieModuleHom.codRestrict H.toLieSubmodule
                ((rootSpace H 0).incl.comp (rootSpaceWeightSpaceProduct R L H L α (-α) 0 ⋯)) ⋯ :
              ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α)) →ₗ⁅R,↥H⁆ ↥H.toLieSubmodule) :
            (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → ↥H)
          m =
        x) ↔
    ∃ (m : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))),
      ((LieModuleHom.codRestrict H.toLieSubmodule
                ((rootSpace H 0).incl.comp (rootSpaceWeightSpaceProduct R L H L α (-α) 0 ⋯)) ⋯ :
              ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α)) →ₗ⁅R,↥H⁆ ↥H.toLieSubmodule) :
            (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → ↥H.toLieSubmodule)
          m =
        x
⊢ x ∈
      (LieModuleHom.codRestrict H.toLieSubmodule ((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯))
          ⋯).range ↔
    (↑x : L) ∈
      LieSubmodule.map H.toLieSubmodule.incl
        (LieModuleHom.codRestrict H.toLieSubmodule ((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯))
            ⋯).range

Tactic:
simp only [rootSpaceProduct_def, LieModuleHom.mem_range, LieSubmodule.mem_map,
      LieSubmodule.incl_apply, SetLike.coe_eq_coe, exists_eq_right]

Premises used: LieModuleHom.mem_range, LieSubmodule.incl_apply, SetLike.coe_eq_coe, LieAlgebra.rootSpaceProduct_def, exists_eq_right, LieSubmodule.mem_map
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
⊢ (∃ (m : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))),
      ((LieModuleHom.codRestrict H.toLieSubmodule
                ((rootSpace H 0).incl.comp (rootSpaceWeightSpaceProduct R L H L α (-α) 0 ⋯)) ⋯ :
              ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α)) →ₗ⁅R,↥H⁆ ↥H.toLieSubmodule) :
            (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → ↥H)
          m =
        x) ↔
    ∃ (m : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))),
      ((LieModuleHom.codRestrict H.toLieSubmodule
                ((rootSpace H 0).incl.comp (rootSpaceWeightSpaceProduct R L H L α (-α) 0 ⋯)) ⋯ :
              ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α)) →ₗ⁅R,↥H⁆ ↥H.toLieSubmodule) :
            (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → ↥H.toLieSubmodule)
          m =
        x

Tactic:
rfl
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
⊢ x ∈ corootSpace α ↔ (↑x : L) ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α)

Tactic:
have : x ∈ corootSpace α ↔
      (x : L) ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α) := by
    rw [corootSpace]
    simp only [rootSpaceProduct_def, LieModuleHom.mem_range, LieSubmodule.mem_map,
      LieSubmodule.incl_apply, SetLike.coe_eq_coe, exists_eq_right]
    rfl
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
this : x ∈ corootSpace α ↔ (↑x : L) ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α)
simp_rw :
  Membership.mem (γ := Submodule R L)
      (Submodule.span R
        {x : L |
          ∃ (a : ↥(rootSpace H α)) (b : ↥(rootSpace H (-α))),
            ((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[R] L) : (a : ↥H.toLieSubmodule) → L)
                (((↑(LieModuleHom.codRestrict H.toLieSubmodule
                            ((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯)) ⋯) :
                        ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α)) →ₗ[R] ↥H.toLieSubmodule) :
                      (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → ↥H.toLieSubmodule)
                    (a ⊗ₜ[R] b) :
                  ↥H.toLieSubmodule) =
              x})
      (↑x : L) ↔
    Membership.mem (γ := Submodule R L)
      (Submodule.span R
        {x : L | ∃ y ∈ (↑(rootSpace H α) : Submodule R L), ∃ z ∈ (↑(rootSpace H (-α)) : Submodule R L), ⁅y, z⁆ = x})
      (↑x : L)
⊢ x ∈ corootSpace α ↔
    Membership.mem (γ := Submodule R L)
      (Submodule.span R {x : L | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}) (↑x : L)

Tactic:
simp_rw [this, corootSpace, ← LieModuleHom.map_top, ← LieSubmodule.mem_toSubmodule,
    LieSubmodule.toSubmodule_map, LieSubmodule.top_toSubmodule, ← TensorProduct.span_tmul_eq_top,
    LinearMap.map_span, Set.image, Set.mem_setOf_eq, exists_exists_exists_and_eq]

Premises used: TensorProduct.span_tmul_eq_top, LieSubmodule.mem_toSubmodule, LieSubmodule.toSubmodule_map, LieSubmodule.top_toSubmodule, exists_exists_exists_and_eq, Set.mem_setOf_eq, LieAlgebra.corootSpace, LinearMap.map_span, Set.image, LieModuleHom.map_top
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
this : x ∈ corootSpace α ↔ (↑x : L) ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α)
change :
  Membership.mem (γ := Submodule R L)
      (Submodule.span R {x : L | ∃ (a : ↥(rootSpace H α)) (b : ↥(rootSpace H (-α))), ⁅(↑a : L), (↑b : L)⁆ = x})
      (↑x : L) ↔
    Membership.mem (γ := Submodule R L)
      (Submodule.span R
        {x : L | ∃ y ∈ (↑(rootSpace H α) : Submodule R L), ∃ z ∈ (↑(rootSpace H (-α)) : Submodule R L), ⁅y, z⁆ = x})
      (↑x : L)
⊢ Membership.mem (γ := Submodule R L)
      (Submodule.span R
        {x : L |
          ∃ (a : ↥(rootSpace H α)) (b : ↥(rootSpace H (-α))),
            ((↑H.toLieSubmodule.incl : ↥H.toLieSubmodule →ₗ[R] L) : (a : ↥H.toLieSubmodule) → L)
                (((↑(LieModuleHom.codRestrict H.toLieSubmodule
                            ((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯)) ⋯) :
                        ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α)) →ₗ[R] ↥H.toLieSubmodule) :
                      (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → ↥H.toLieSubmodule)
                    (a ⊗ₜ[R] b) :
                  ↥H.toLieSubmodule) =
              x})
      (↑x : L) ↔
    Membership.mem (γ := Submodule R L)
      (Submodule.span R
        {x : L | ∃ y ∈ (↑(rootSpace H α) : Submodule R L), ∃ z ∈ (↑(rootSpace H (-α)) : Submodule R L), ⁅y, z⁆ = x})
      (↑x : L)

Tactic:
change (x : L) ∈ Submodule.span R
    {x | ∃ (a : rootSpace H α) (b : rootSpace H (-α)), ⁅(a : L), (b : L)⁆ = x} ↔ _

Premises used: Bracket.bracket, setOf, Exists, Submodule.span, Subtype.val, Eq
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
this : x ∈ corootSpace α ↔ (↑x : L) ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α)
⊢ Membership.mem (γ := Submodule R L)
      (Submodule.span R {x : L | ∃ (a : ↥(rootSpace H α)) (b : ↥(rootSpace H (-α))), ⁅(↑a : L), (↑b : L)⁆ = x})
      (↑x : L) ↔
    Membership.mem (γ := Submodule R L)
      (Submodule.span R
        {x : L | ∃ y ∈ (↑(rootSpace H α) : Submodule R L), ∃ z ∈ (↑(rootSpace H (-α)) : Submodule R L), ⁅y, z⁆ = x})
      (↑x : L)

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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
set :
  let s : Set ↥H := {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)};
  x ∈ corootSpace α ↔ Membership.mem (γ := Submodule R ↥H) (Submodule.span R s) x
⊢ x ∈ corootSpace α ↔
    Membership.mem (γ := Submodule R ↥H)
      (Submodule.span R {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}) x

Tactic:
set s : Set H := ({⁅y, z⁆ | (y ∈ rootSpace H α) (z ∈ rootSpace H (-α))} : Set H)

Premises used: Bracket.bracket, setOf, Membership.mem, Exists, Subtype, And, LieAlgebra.rootSpace, Subtype.val, Eq, Neg.neg, Set
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
this :
  Eq (α := Set L) ((⇑H.subtype : (a : ↥H.toSubmodule) → L) '' s)
    {x : L | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}
erw :
  x ∈ corootSpace α ↔
    Membership.mem (α := L) (γ := Set L)
      ((⇑H.subtype : (a : ↥H.toSubmodule) → L) '' (↑(Submodule.span R s) : Set ↥H.toSubmodule))
      ((H.subtype : (a : ↥H.toSubmodule) → L) x : L)
⊢ x ∈ corootSpace α ↔ Membership.mem (γ := Submodule R ↥H) (Submodule.span R s) x

Tactic:
erw [← (H : Submodule R L).injective_subtype.mem_set_image (s := Submodule.span R s)]

Premises used: Submodule.injective_subtype, LieSubalgebra.toSubmodule, Function.Injective.mem_set_image
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
this :
  Eq (α := Set L) ((⇑H.subtype : (a : ↥H.toSubmodule) → L) '' s)
    {x : L | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}
rw :
  x ∈ corootSpace α ↔
    Membership.mem (α := L) (Submodule.map H.subtype (Submodule.span R s))
      ((H.subtype : (a : ↥H.toSubmodule) → L) x : L)
rw₁ : x ∈ corootSpace α ↔ (↑x : L) ∈ Submodule.map H.subtype (Submodule.span R s)
rw₂ :
  x ∈ corootSpace α ↔
    Membership.mem (γ := Submodule R L) (Submodule.span R ((⇑H.subtype : (a : ↥H.toSubmodule) → L) '' s)) (↑x : L)
rw₃ :
  Membership.mem (γ := Submodule R L)
      (Submodule.span R {x : L | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}) (↑x : L) ↔
    Membership.mem (γ := Submodule R L) (Submodule.span R ((⇑H.subtype : (a : ↥H.toSubmodule) → L) '' s)) (↑x : L)
rw₄ rw₅ :
  Membership.mem (γ := Submodule R L) (Submodule.span R ((⇑H.subtype : (a : ↥H.toSubmodule) → L) '' s)) (↑x : L) ↔
    Membership.mem (γ := Submodule R L) (Submodule.span R ((⇑H.subtype : (a : ↥H.toSubmodule) → L) '' s)) (↑x : L)
⊢ x ∈ corootSpace α ↔
    ∃ (x_1 : ↥H.toSubmodule),
      Membership.mem (γ := Submodule R ↥H) (Submodule.span R s) x_1 ∧
        Eq (α := L) ((H.subtype : (a : ↥H.toSubmodule) → L) x_1 : L) ((H.subtype : (a : ↥H.toSubmodule) → L) x : L)

Tactic:
rw [← Submodule.mem_map, Submodule.coe_subtype, Submodule.map_span, mem_corootSpace, ← this]

Premises used: Submodule.mem_map, Submodule.coe_subtype, Submodule.map_span, LieAlgebra.mem_corootSpace
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
suffices :
  Eq (α := Set L) ((⇑H.subtype : (a : ↥H.toSubmodule) → L) '' s)
    {x : L | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}
⊢ x ∈ corootSpace α ↔ Membership.mem (γ := Submodule R ↥H) (Submodule.span R s) x

Tactic:
suffices H.subtype '' s = {⁅y, z⁆ | (y ∈ rootSpace H α) (z ∈ rootSpace H (-α))} by
    erw [← (H : Submodule R L).injective_subtype.mem_set_image (s := Submodule.span R s)]
    rw [mem_image]
    simp_rw [SetLike.mem_coe]
    rw [← Submodule.mem_map, Submodule.coe_subtype, Submodule.map_span, mem_corootSpace, ← this]
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
h :
  ∀ (u : L),
    Membership.mem (γ := Set L) ((⇑H.subtype : (a : ↥H.toSubmodule) → L) '' s) u ↔
      Membership.mem (γ := Set L) {x : L | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x} u
⊢ Eq (α := Set L) ((⇑H.subtype : (a : ↥H.toSubmodule) → L) '' s)
    {x : L | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}

Tactic:
ext u
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
u : L
h :
  (∃ (x : u ∈ H),
      Membership.mem (γ := Set ↥H.toSubmodule) {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
        (Subtype.mk (p := fun (a : L) ↦ a ∈ H.toSubmodule) u ⋯)) ↔
    ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u
⊢ Membership.mem (γ := Set L) ((⇑H.subtype : (a : ↥H.toSubmodule) → L) '' s) u ↔
    Membership.mem (γ := Set L) {x : L | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x} u

Tactic:
simp only [Submodule.coe_subtype, mem_image, Subtype.exists, LieSubalgebra.mem_toSubmodule,
    exists_and_right, exists_eq_right, mem_setOf_eq, s]

Premises used: LieSubalgebra.mem_toSubmodule, Set.mem_image, Subtype.exists, exists_eq_right, Set.mem_setOf_eq, exists_and_right, Submodule.coe_subtype
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
u : L
⊢ (∃ (x : u ∈ H),
      Membership.mem (γ := Set ↥H.toSubmodule) {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
        (Subtype.mk (p := fun (a : L) ↦ a ∈ H.toSubmodule) u ⋯)) ↔
    ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u

Tactic:
⟨fun ⟨_, y, hy, z, hz, hyz⟩ ↦ ⟨y, hy, z, hz, hyz⟩,
    fun ⟨y, hy, z, hz, hyz⟩ ↦ ⟨?_, y, hy, z, hz, hyz⟩⟩

Premises used: Iff.mpr, Iff.of_eq, _private.0.LieAlgebra.mem_corootSpace'.match_5, Bracket.bracket, setOf, Membership.mem, Exists, _private.0.LieAlgebra.mem_corootSpace'._simp_4, Subtype.mk, And, And.intro, LieAlgebra.rootSpace, Iff.intro, Exists.intro, Subtype.val, Eq, Neg.neg, _private.0.LieAlgebra.mem_corootSpace'.match_6
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
u : L
h :
  (∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u) →
    ∀ (y : L) (hy : y ∈ rootSpace H α) (z : L) (hz : z ∈ rootSpace H (-α)) (hyz : ⁅y, z⁆ = u), u ∈ H
⊢ (∃ (x : u ∈ H),
      Membership.mem (γ := Set ↥H.toSubmodule) {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
        (Subtype.mk (p := fun (a : L) ↦ a ∈ H.toSubmodule) u ⋯)) ↔
    ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u

Tactic:
refine ⟨fun ⟨_, y, hy, z, hz, hyz⟩ ↦ ⟨y, hy, z, hz, hyz⟩,
    fun ⟨y, hy, z, hz, hyz⟩ ↦ ⟨?_, y, hy, z, hz, hyz⟩⟩
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
u : L
h : ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = u
⊢ (↑((rootSpaceProduct R L H α (-α) 0 ⋯ : (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → ↥(rootSpace H 0))
          (Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H α) y hy ⊗ₜ[R]
            Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (-α)) z hz)) :
      L) ∈
    rootSpace H 0

Tactic:
(rootSpaceProduct R L H α (-α) 0 (add_neg_cancel α) (⟨y, hy⟩ ⊗ₜ[R] ⟨z, hz⟩)).property

Premises used: add_neg_cancel, Subtype.mk, LieAlgebra.rootSpaceProduct, TensorProduct.tmul, OfNat.ofNat, DFunLike.coe, Neg.neg, Subtype.property
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
u : L
h : ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = u
a :
  u ∈ H ↔
    (↑((rootSpaceProduct R L H α (-α) 0 ⋯ : (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → ↥(rootSpace H 0))
            (Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H α) y hy ⊗ₜ[R]
              Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (-α)) z hz)) :
        L) ∈
      rootSpace H 0
⊢ u ∈ H

Tactic:
convert!
    (rootSpaceProduct R L H α (-α) 0 (add_neg_cancel α) (⟨y, hy⟩ ⊗ₜ[R] ⟨z, hz⟩)).property using 0

Premises used: add_neg_cancel, Subtype.mk, LieAlgebra.rootSpaceProduct, TensorProduct.tmul, OfNat.ofNat, DFunLike.coe, Neg.neg, Subtype.property
-- 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
inst_4 : H.IsCartanSubalgebra
inst_5 : IsNoetherian R L
α : ↥H → R
x : ↥H
s : Set ↥H := {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}
u : L
h : ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = u
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = u
⊢ u ∈ H ↔
    (↑((rootSpaceProduct R L H α (-α) 0 ⋯ : (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → ↥(rootSpace H 0))
            (Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H α) y hy ⊗ₜ[R]
              Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (-α)) z hz)) :
        L) ∈
      rootSpace H 0

Tactic:
simp [hyz]
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
I : LieIdeal K L
⊢ LieSubmodule.restr I H = ⨆ (χ : Weight K (↥H) L), LieSubmodule.restr I H ⊓ genWeightSpace L (⇑χ : (a : ↥H) → K)

Tactic:
eq_iSup_inf_genWeightSpace (N := I.restr H)

Premises used: LieSubmodule.restr, Set.Mem, setOf, LieModule.eq_iSup_inf_genWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
L : Type u_2
inst : LieRing L
K : Type u_4
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsTriangularizable K (↥H) L
I : LieIdeal K L
⊢ LieSubmodule.restr I H =
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)

Tactic:
le_antisymm ?_ (sup_le inf_le_left (iSup₂_le fun _ _ ↦ inf_le_left))

Premises used: iSup₂_le, le_antisymm, sup_le, inf_le_left