awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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
x y : L
hy : y ∈ H
hx :
  ∀ (y_1 : ↥H),
    ∃ (k : ℕ),
      Eq (α := L)
        ((HPow.hPow (α := Module.End R L) ((toEnd R (↥H) L : (a : ↥H) → Module.End R L) y_1 : Module.End R L) k :
              (a : L) → L)
            ⁅x, y⁆ :
          L)
        (0 : L)
k : ℕ
hk :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L)
            ((toEnd R (↥H) L : (a : ↥H) → Module.End R L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy) : Module.End R L)
            k :
          (a : L) → L)
        ⁅y, x⁆ :
      L)
    (0 : L)
h :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L)
              ((toEnd R (↥H) L : (a : ↥H) → Module.End R L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy) :
                Module.End R L)
              k ∘ₗ
            (toEnd R (↥H) L : (a : ↥H) → Module.End R L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy) :
          (a : L) → L)
        x :
      L)
    (0 : L)
h₁ :
  Eq (α := L)
    (Function.comp (β := L)
      (⇑(HPow.hPow (α := Module.End R L)
            ((toEnd R (↥H) L : (a : ↥H) → Module.End R L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy) : Module.End R L)
            k) :
        (a : L) → L)
      (⇑((toEnd R (↥H) L : (a : ↥H) → Module.End R L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy) : Module.End R L) :
        (a : L) → L)
      x)
    0
h₂ :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L)
            ((toEnd R (↥H) L : (a : ↥H) → Module.End R L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy) : Module.End R L)
            k :
          (a : L) → L)
        ((((toEnd R (↥H) L : (a : ↥H) → Module.End R L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy) : Module.End R L) :
              (a : L) → L)
            x :
          L) :
      L)
    (0 : L)
h₃ :
  Eq (α := L)
    ((HPow.hPow (α := Module.End R L)
            ((toEnd R (↥H) L : (a : ↥H) → Module.End R L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy) : Module.End R L)
            k :
          (a : L) → L)
        ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy, x⁆ :
      L)
    (0 : L)
⊢ Eq (α := L)
    ((HPow.hPow (α := Module.End R L)
            ((toEnd R (↥H) L : (a : ↥H) → Module.End R L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy) : Module.End R L)
            (k + 1) :
          (a : L) → L)
        x :
      L)
    (0 : L)
have h₄ : Eq (α := L)
  ((HPow.hPow (α := Module.End R L)
          ((toEnd R (↥H) L : (a : ↥H) → Module.End R L) (Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy) : Module.End R L)
          k :
        (a : L) → L)
      ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy) : L), x⁆ :
    L)
  (0 : L)
Tactic: rw [Module.End.iterate_succ, LinearMap.coe_comp, Function.comp_apply, toEnd_apply_apply,
    LieSubalgebra.coe_bracket_of_module, Submodule.coe_mk, hk]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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
h : zeroRootSubalgebra R L H = H
⊢ H.normalizer = H
have rw : (zeroRootSubalgebra R L H).normalizer = zeroRootSubalgebra R L H
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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
⊢ zeroRootSubalgebra R L H = H
have refine : zeroRootSubalgebra R L H ≤ H
Tactic: refine le_antisymm ?_ (le_zeroRootSubalgebra R L H)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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
⊢ zeroRootSubalgebra R L H ≤ H
have suffices : rootSpace H 0 ≤ H.toLieSubmodule
Tactic: suffices rootSpace H 0 ≤ H.toLieSubmodule by exact fun x hx => this hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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
⊢ rootSpace H 0 ≤ H.toLieSubmodule
have obtain : ∀ (k : ℕ) (hk : rootSpace H 0 ≤ LieSubmodule.ucs k ⊥), rootSpace H 0 ≤ H.toLieSubmodule
Tactic: obtain ⟨k, hk⟩ := (rootSpace H 0).isNilpotent_iff_exists_self_le_ucs.mp (by infer_instance)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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 : IsNoetherian R L
⊢ H.toLieSubmodule = rootSpace H 0 ↔ H.IsCartanSubalgebra
have rw : (↑H.toLieSubmodule : Submodule R L) = (↑(rootSpace H 0) : Submodule R L) ↔
  (zeroRootSubalgebra R L H).toSubmodule = H.toSubmodule
Tactic: rw [← zeroRootSubalgebra_eq_iff_is_cartan, ← LieSubalgebra.toSubmodule_inj,
    ← LieSubmodule.toSubmodule_inj]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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
⊢ rootSpace H 0 = H.toLieSubmodule
have rw : (↑(rootSpace H 0) : Submodule R L) = (↑H.toLieSubmodule : Submodule R L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, ← coe_zeroRootSubalgebra,
    zeroRootSubalgebra_eq_of_is_cartan R L H, LieSubalgebra.coe_toLieSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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)
⊢ rootSpace H 0 = H.toLieSubmodule
have rw₁ : (zeroRootSubalgebra R L H).toSubmodule = (↑H.toLieSubmodule : Submodule R L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, ← coe_zeroRootSubalgebra,
    zeroRootSubalgebra_eq_of_is_cartan R L H, LieSubalgebra.coe_toLieSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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)
⊢ rootSpace H 0 = H.toLieSubmodule
have rw₂ : H.toSubmodule = (↑H.toLieSubmodule : Submodule R L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, ← coe_zeroRootSubalgebra,
    zeroRootSubalgebra_eq_of_is_cartan R L H, LieSubalgebra.coe_toLieSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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)
⊢ rootSpace H 0 = H.toLieSubmodule
have rw₃ : H.toSubmodule = H.toSubmodule
Tactic: rw [← LieSubmodule.toSubmodule_inj, ← coe_zeroRootSubalgebra,
    zeroRootSubalgebra_eq_of_is_cartan R L H, LieSubalgebra.coe_toLieSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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) H.toLieSubmodule
      (((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 ⋯) :
            (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → L)
          m :
        L)
have rw : ∀ (m : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))),
  Membership.mem (α := L) (rootSpace H 0)
    (((rootSpace H 0).incl.comp (rootSpaceProduct R L H α (-α) 0 sorry) :
          (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → L)
        m :
      L)
Tactic: rw [← rootSpace_zero_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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 ∈
      (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
have simp : (∃ (m : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))),
    ((LieModuleHom.codRestrict H.toLieSubmodule
              ((rootSpace H 0).incl.comp (rootSpaceWeightSpaceProduct R L H L α (-α) 0 sorry)) sorry :
            ↥(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 sorry)) sorry :
            ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α)) →ₗ⁅R,↥H⁆ ↥H.toLieSubmodule) :
          (a : ↥(rootSpace H α) ⊗[R] ↥(rootSpace H (-α))) → ↥H.toLieSubmodule)
        m =
      x
Tactic: simp only [rootSpaceProduct_def, LieModuleHom.mem_range, LieSubmodule.mem_map,
      LieSubmodule.incl_apply, SetLike.coe_eq_coe, exists_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (hypothesis)
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 α ↔
    Membership.mem (γ := Submodule R L)
      (Submodule.span R {x : L | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}) (↑x : L)
have this : 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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 α)
⊢ x ∈ corootSpace α ↔
    Membership.mem (γ := Submodule R L)
      (Submodule.span R {x : L | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}) (↑x : L)
have 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 sorry)) sorry) :
                      ↥(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: 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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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 (-α))),
            ((↑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)
have 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)
Tactic: change (x : L) ∈ Submodule.span R
    {x | ∃ (a : rootSpace H α) (b : rootSpace H (-α)), ⁅(a : L), (b : L)⁆ = x} ↔ _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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}
⊢ x ∈ corootSpace α ↔ Membership.mem (γ := Submodule R ↥H) (Submodule.span R s) x
have 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)
Tactic: erw [← (H : Submodule R L).injective_subtype.mem_set_image (s := Submodule.span R s)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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}
⊢ 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)
have rw : x ∈ corootSpace α ↔
  Membership.mem (α := L) (Submodule.map H.subtype (Submodule.span R s)) ((H.subtype : (a : ↥H.toSubmodule) → L) x : L)
Tactic: rw [← Submodule.mem_map, Submodule.coe_subtype, Submodule.map_span, mem_corootSpace, ← this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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)
⊢ 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)
have rw₁ : x ∈ corootSpace α ↔ (↑x : L) ∈ Submodule.map H.subtype (Submodule.span R s)
Tactic: rw [← Submodule.mem_map, Submodule.coe_subtype, Submodule.map_span, mem_corootSpace, ← this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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)
⊢ 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)
have rw₂ : x ∈ corootSpace α ↔
  Membership.mem (γ := Submodule R L) (Submodule.span R ((⇑H.subtype : (a : ↥H.toSubmodule) → L) '' s)) (↑x : L)
Tactic: rw [← Submodule.mem_map, Submodule.coe_subtype, Submodule.map_span, mem_corootSpace, ← this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← Submodule.mem_map, Submodule.coe_subtype, Submodule.map_span, mem_corootSpace, ← this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← Submodule.mem_map, Submodule.coe_subtype, Submodule.map_span, mem_corootSpace, ← this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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)}
⊢ x ∈ corootSpace α ↔ Membership.mem (γ := Submodule R ↥H) (Submodule.span R s) x
have suffices : Eq (α := Set L) ((⇑H.subtype : (a : ↥H.toSubmodule) → L) '' s)
  {x : L | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = 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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Cartan (goal)
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)}
⊢ Eq (α := Set L) ((⇑H.subtype : (a : ↥H.toSubmodule) → L) '' s)
    {x : L | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = x}
have 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
Tactic: ext u