awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
hLK : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : (↑{x : LieSubalgebra K L | ∃ x_1 ∈ U, engel K x_1 = x} : Type u_2) :=
  Subtype.mk (p := fun (x : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L)) {x : LieSubalgebra K L | ∃ x_1 ∈ U, engel K x_1 = x} x) (engel K x) ⋯
Ey : (↑{x : LieSubalgebra K L | ∃ y ∈ U, engel K y = x} : Type u_2) :=
  Subtype.mk (p := fun (x : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L)) {x : LieSubalgebra K L | ∃ y ∈ U, engel K y = x} x) (engel K y) ⋯
hUle : U ≤ (↑Ex : LieSubalgebra K L)
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src : LieSubalgebra K L := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank.{u_1, u_2} K ↥E
hr : r < finrank K L
x' : ↥U := Subtype.mk (p := fun (x : L) ↦ x ∈ U) x hxU
y' : ↥U := Subtype.mk (p := fun (x : L) ↦ x ∈ U) y hyU
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : Ne (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
s : Finset K
hs : r ≤ s.card
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : Membership.mem (γ := LieSubalgebra K L) (engel K (↑v : L)) z
z' : Q := (LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z
hz' :
  ∃ (n : ℕ),
    Eq (α := Q) ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) n : (a : Q) → Q) z' : Q)
      (0 : Q)
n : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    Eq (α := Q) ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) n : (a : Q) → Q) z' : Q)
      (0 : Q))
    hz'
_hn :
  n =
    Nat.find (p := fun (n : ℕ) ↦
      Eq (α := Q)
        ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) n : (a : Q) → Q) z' : Q) (0 : Q))
      hz'
hn :
  Eq (α := Q) ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) n : (a : Q) → Q) z' : Q)
    (0 : Q)
k : ℕ
hk : n = k + 1
hsψ : z' ≠ 0
h :
  Eq (α := Q)
    ((((toEnd K (↥U) Q : (a : ↥U) → End K Q) (α • u + x') : End K Q) : (a : Q) → Q)
        ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) k : (a : Q) → Q) z') :
      Q)
    ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) n : (a : Q) → Q) z' : Q)
⊢ Eq (α := Q)
    ((((toEnd K (↥U) Q : (a : ↥U) → End K Q) (α • u + x') : End K Q) : (a : Q) → Q)
        ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) k : (a : Q) → Q) z') :
      Q)
    (0 : Q)
have h₁ : Eq (α := Q)
  ((((toEnd K (↥U) Q : (a : ↥U) → End K Q) (α • u + x') : End K Q) : (a : Q) → Q)
      ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) k : (a : Q) → Q) z') :
    Q)
  ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) (k + 1) : (a : Q) → Q) z' : Q)
Tactic: rw [← hn, hk, pow_succ', Module.End.mul_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
⊢ ∃ (x : L), IsCartanSubalgebra (engel K x)
have obtain : ∀ (x : L) (hx : IsRegular K x), ∃ (x : L), IsCartanSubalgebra (engel K x)
Tactic: obtain ⟨x, hx⟩ := exists_isRegular_of_finrank_le_card K L h
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
⊢ ∃ (x : L), IsCartanSubalgebra (engel K x)
have h₁ : IsCartanSubalgebra (engel K x)
Tactic: use x
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
⊢ IsCartanSubalgebra (engel K x)
have h₁ : LieRing.IsNilpotent.{u_2} ↥(engel K x)
Tactic: refine ⟨?_, normalizer_engel _ _⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
⊢ LieRing.IsNilpotent.{u_2} ↥(engel K x)
have h₁ : ∀ (x_1 : L),
  Membership.mem (γ := LieSubalgebra K L) (engel K x) x_1 → LE.le (α := LieSubalgebra K L) (engel K x) (engel K x_1)
Tactic: apply isNilpotent_of_forall_le_engel
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
y : L
hy : Membership.mem (γ := LieSubalgebra K L) (engel K x) y
Ex : (↑{x_1 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_1} :
  Type u_2) :=
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L))
      {x_2 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_2}
      x_1)
    (engel K x) ⋯
⊢ LE.le (α := LieSubalgebra K L) (engel K x) (engel K y)
have h₁ : IsBot Ex
Tactic: suffices IsBot Ex from @this ⟨engel K y, y, hy, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
y : L
hy : Membership.mem (γ := LieSubalgebra K L) (engel K x) y
Ex : (↑{x_1 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_1} :
  Type u_2) :=
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L))
      {x_2 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_2}
      x_1)
    (engel K x) ⋯
⊢ IsBot Ex
have h₁ : IsMin Ex
Tactic: apply engel_isBot_of_isMin h (engel K x) Ex le_rfl
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
y_1 : L
hy_1 : Membership.mem (γ := LieSubalgebra K L) (engel K x) y_1
Ex : (↑{x_1 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_1} :
  Type u_2) :=
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L))
      {x_2 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_2}
      x_1)
    (engel K x) ⋯
y : L
hy : Membership.mem (γ := LieSubalgebra K L) (engel K x) y
hyx :
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
      Membership.mem (γ := Set (LieSubalgebra K L))
        {x_2 : LieSubalgebra K L |
          ∃ (x_3 : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) x_3 ∧ engel K x_3 = x_2}
        x_1)
      (engel K y) ⋯ ≤
    Ex
this : finrank.{u_1, u_2} K ↥(engel K x) ≤ finrank.{u_1, u_2} K ↥(engel K y)
⊢ Ex ≤
    Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
      Membership.mem (γ := Set (LieSubalgebra K L))
        {x_2 : LieSubalgebra K L |
          ∃ (x_3 : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) x_3 ∧ engel K x_3 = x_2}
        x_1)
      (engel K y) ⋯
have suffices : Eq (α := LieSubalgebra K L) (engel K y) (engel K x)
Tactic: suffices engel K y = engel K x from this.ge
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
y_1 : L
hy_1 : Membership.mem (γ := LieSubalgebra K L) (engel K x) y_1
Ex : (↑{x_1 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_1} :
  Type u_2) :=
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L))
      {x_2 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_2}
      x_1)
    (engel K x) ⋯
y : L
hy : Membership.mem (γ := LieSubalgebra K L) (engel K x) y
hyx :
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
      Membership.mem (γ := Set (LieSubalgebra K L))
        {x_2 : LieSubalgebra K L |
          ∃ (x_3 : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) x_3 ∧ engel K x_3 = x_2}
        x_1)
      (engel K y) ⋯ ≤
    Ex
this : finrank.{u_1, u_2} K ↥(engel K x) ≤ finrank.{u_1, u_2} K ↥(engel K y)
⊢ Eq (α := LieSubalgebra K L) (engel K y) (engel K x)
have a : Eq (α := Submodule K L) (LieSubalgebra.toSubmodule (engel K y)) (LieSubalgebra.toSubmodule (engel K x))
Tactic: apply LieSubalgebra.toSubmodule_injective
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
y_1 : L
hy_1 : Membership.mem (γ := LieSubalgebra K L) (engel K x) y_1
Ex : (↑{x_1 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_1} :
  Type u_2) :=
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L))
      {x_2 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_2}
      x_1)
    (engel K x) ⋯
y : L
hy : Membership.mem (γ := LieSubalgebra K L) (engel K x) y
hyx :
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
      Membership.mem (γ := Set (LieSubalgebra K L))
        {x_2 : LieSubalgebra K L |
          ∃ (x_3 : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) x_3 ∧ engel K x_3 = x_2}
        x_1)
      (engel K y) ⋯ ≤
    Ex
⊢ Ex ≤
    Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
      Membership.mem (γ := Set (LieSubalgebra K L))
        {x_2 : LieSubalgebra K L |
          ∃ (x_3 : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) x_3 ∧ engel K x_3 = x_2}
        x_1)
      (engel K y) ⋯
have h₁ : finrank.{u_1, u_2} K ↥(engel K x) ≤ finrank.{u_1, u_2} K ↥(engel K y)
Tactic: suffices finrank K (engel K x) ≤ finrank K (engel K y) by
    suffices engel K y = engel K x from this.ge
    apply LieSubalgebra.toSubmodule_injective
    exact Submodule.eq_of_le_of_finrank_le hyx this
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
y_1 : L
hy_1 : Membership.mem (γ := LieSubalgebra K L) (engel K x) y_1
Ex : (↑{x_1 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_1} :
  Type u_2) :=
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L))
      {x_2 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_2}
      x_1)
    (engel K x) ⋯
y : L
hy : Membership.mem (γ := LieSubalgebra K L) (engel K x) y
hyx :
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
      Membership.mem (γ := Set (LieSubalgebra K L))
        {x_2 : LieSubalgebra K L |
          ∃ (x_3 : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) x_3 ∧ engel K x_3 = x_2}
        x_1)
      (engel K y) ⋯ ≤
    Ex
⊢ finrank.{u_1, u_2} K ↥(engel K x) ≤ finrank.{u_1, u_2} K ↥(engel K y)
have h₁ : rank K L ≤ finrank.{u_1, u_2} K ↥(engel K y)
Tactic: rw [(isRegular_iff_finrank_engel_eq_rank K x).mp hx]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
inst_4 : Infinite K
⊢ ∃ (x : L), IsCartanSubalgebra (engel K x)
have h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
Tactic: apply exists_isCartanSubalgebra_engel_of_finrank_le_card
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : H.IsCartanSubalgebra
⊢ H.toLieSubmodule.normalizer = H.toLieSubmodule
have rw : (↑H.toLieSubmodule.normalizer : Submodule R L) = (↑H.toLieSubmodule : Submodule R L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, coe_normalizer_eq_normalizer,
    IsCartanSubalgebra.self_normalizing, coe_toLieSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : H.IsCartanSubalgebra
rw : (↑H.toLieSubmodule.normalizer : Submodule R L) = (↑H.toLieSubmodule : Submodule R L)
⊢ H.toLieSubmodule.normalizer = H.toLieSubmodule
have rw₁ : H.normalizer.toSubmodule = (↑H.toLieSubmodule : Submodule R L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, coe_normalizer_eq_normalizer,
    IsCartanSubalgebra.self_normalizing, coe_toLieSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : H.IsCartanSubalgebra
rw : (↑H.toLieSubmodule.normalizer : Submodule R L) = (↑H.toLieSubmodule : Submodule R L)
rw₁ : H.normalizer.toSubmodule = (↑H.toLieSubmodule : Submodule R L)
⊢ H.toLieSubmodule.normalizer = H.toLieSubmodule
have rw₂ : H.toSubmodule = (↑H.toLieSubmodule : Submodule R L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, coe_normalizer_eq_normalizer,
    IsCartanSubalgebra.self_normalizing, coe_toLieSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : H.IsCartanSubalgebra
rw : (↑H.toLieSubmodule.normalizer : Submodule R L) = (↑H.toLieSubmodule : Submodule R L)
rw₁ : H.normalizer.toSubmodule = (↑H.toLieSubmodule : Submodule R L)
rw₂ : H.toSubmodule = (↑H.toLieSubmodule : Submodule R L)
⊢ H.toLieSubmodule.normalizer = H.toLieSubmodule
have rw₃ : H.toSubmodule = H.toSubmodule
Tactic: rw [← LieSubmodule.toSubmodule_inj, coe_normalizer_eq_normalizer,
    IsCartanSubalgebra.self_normalizing, coe_toLieSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : H.IsCartanSubalgebra
k : ℕ
⊢ LieSubmodule.ucs k H.toLieSubmodule = H.toLieSubmodule
have zero : LieSubmodule.ucs 0 H.toLieSubmodule = H.toLieSubmodule
Tactic: induction k with
  | zero => simp
  | succ k ih => simp [ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : H.IsCartanSubalgebra
k : ℕ
zero : LieSubmodule.ucs 0 H.toLieSubmodule = H.toLieSubmodule
⊢ LieSubmodule.ucs k H.toLieSubmodule = H.toLieSubmodule
have succ : ∀ (k : ℕ) (ih : LieSubmodule.ucs k H.toLieSubmodule = H.toLieSubmodule),
  LieSubmodule.ucs (k + 1) H.toLieSubmodule = H.toLieSubmodule
Tactic: induction k with
  | zero => simp
  | succ k ih => simp [ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
⊢ H.IsCartanSubalgebra ↔ H.toLieSubmodule.IsUcsLimit
have mp : H.IsCartanSubalgebra → H.toLieSubmodule.IsUcsLimit
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
mp : H.IsCartanSubalgebra → H.toLieSubmodule.IsUcsLimit
⊢ H.IsCartanSubalgebra ↔ H.toLieSubmodule.IsUcsLimit
have mpr : H.toLieSubmodule.IsUcsLimit → H.IsCartanSubalgebra
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h : H.IsCartanSubalgebra
⊢ H.toLieSubmodule.IsUcsLimit
have h₁ : LieRing.IsNilpotent.{v} ↥H
Tactic: have h₁ : LieRing.IsNilpotent H := by infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h : H.IsCartanSubalgebra
h₁ : LieRing.IsNilpotent.{v} ↥H
⊢ H.toLieSubmodule.IsUcsLimit
have mp : ∀ (k : ℕ) (hk : H.toLieSubmodule ≤ LieSubmodule.ucs k ⊥), H.toLieSubmodule.IsUcsLimit
Tactic: obtain ⟨k, hk⟩ := H.toLieSubmodule.isNilpotent_iff_exists_self_le_ucs.mp h₁
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h : H.IsCartanSubalgebra
h₁ : LieRing.IsNilpotent.{v} ↥H
k : ℕ
hk : H.toLieSubmodule ≤ LieSubmodule.ucs k ⊥
⊢ H.toLieSubmodule.IsUcsLimit
have hk₁ : H.toLieSubmodule = LieSubmodule.ucs k ⊥
Tactic: replace hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥ :=
      le_antisymm hk
        (LieSubmodule.ucs_le_of_normalizer_eq_self H.normalizer_eq_self_of_isCartanSubalgebra k)
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h : H.IsCartanSubalgebra
h₁ : LieRing.IsNilpotent.{v} ↥H
k : ℕ
hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥
⊢ H.toLieSubmodule.IsUcsLimit
have mp : ∀ (l : ℕ) (hl : k ≤ l), LieSubmodule.ucs l ⊥ = H.toLieSubmodule
Tactic: refine ⟨k, fun l hl => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h : H.IsCartanSubalgebra
h₁ : LieRing.IsNilpotent.{v} ↥H
k : ℕ
hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥
l : ℕ
hl : k ≤ l
⊢ LieSubmodule.ucs l ⊥ = H.toLieSubmodule
have mp : LieSubmodule.ucs (l - k + k) ⊥ = H.toLieSubmodule
Tactic: rw [← Nat.sub_add_cancel hl, LieSubmodule.ucs_add, ← hk,
      LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h : H.IsCartanSubalgebra
h₁ : LieRing.IsNilpotent.{v} ↥H
k : ℕ
hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥
l : ℕ
hl : k ≤ l
mp : LieSubmodule.ucs (l - k + k) ⊥ = H.toLieSubmodule
⊢ LieSubmodule.ucs l ⊥ = H.toLieSubmodule
have mp₁ : LieSubmodule.ucs (l - k) (LieSubmodule.ucs k ⊥) = H.toLieSubmodule
Tactic: rw [← Nat.sub_add_cancel hl, LieSubmodule.ucs_add, ← hk,
      LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h : H.IsCartanSubalgebra
h₁ : LieRing.IsNilpotent.{v} ↥H
k : ℕ
hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥
l : ℕ
hl : k ≤ l
mp : LieSubmodule.ucs (l - k + k) ⊥ = H.toLieSubmodule
mp₁ : LieSubmodule.ucs (l - k) (LieSubmodule.ucs k ⊥) = H.toLieSubmodule
⊢ LieSubmodule.ucs l ⊥ = H.toLieSubmodule
have mp₂ : LieSubmodule.ucs (l - k) H.toLieSubmodule = H.toLieSubmodule
Tactic: rw [← Nat.sub_add_cancel hl, LieSubmodule.ucs_add, ← hk,
      LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h : H.IsCartanSubalgebra
h₁ : LieRing.IsNilpotent.{v} ↥H
k : ℕ
hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥
l : ℕ
hl : k ≤ l
mp : LieSubmodule.ucs (l - k + k) ⊥ = H.toLieSubmodule
mp₁ : LieSubmodule.ucs (l - k) (LieSubmodule.ucs k ⊥) = H.toLieSubmodule
mp₂ : LieSubmodule.ucs (l - k) H.toLieSubmodule = H.toLieSubmodule
⊢ LieSubmodule.ucs l ⊥ = H.toLieSubmodule
have mp₃ : H.toLieSubmodule = H.toLieSubmodule
Tactic: rw [← Nat.sub_add_cancel hl, LieSubmodule.ucs_add, ← hk,
      LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
⊢ LieModule.IsNilpotent.{v, v} ↥H ↥H
have erw : ∃ (k : ℕ), LieSubmodule.lcs k H.toLieSubmodule = ⊥
Tactic: erw [H.toLieSubmodule.isNilpotent_iff_exists_lcs_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
⊢ ∃ (k : ℕ), LieSubmodule.lcs k H.toLieSubmodule = ⊥
have h : LieSubmodule.lcs k H.toLieSubmodule = ⊥
Tactic: use k
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
⊢ LieSubmodule.lcs k H.toLieSubmodule = ⊥
have h : LieSubmodule.lcs k H.toLieSubmodule ≤ ⊥
Tactic: rw [_root_.eq_bot_iff, LieSubmodule.lcs_le_iff, hk k (le_refl k)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
h : LieSubmodule.lcs k H.toLieSubmodule ≤ ⊥
⊢ LieSubmodule.lcs k H.toLieSubmodule = ⊥
have h₁ : H.toLieSubmodule ≤ LieSubmodule.ucs k ⊥
Tactic: rw [_root_.eq_bot_iff, LieSubmodule.lcs_le_iff, hk k (le_refl k)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
h : LieSubmodule.lcs k H.toLieSubmodule ≤ ⊥
h₁ : H.toLieSubmodule ≤ LieSubmodule.ucs k ⊥
⊢ LieSubmodule.lcs k H.toLieSubmodule = ⊥
have h₂ : H.toLieSubmodule ≤ H.toLieSubmodule
Tactic: rw [_root_.eq_bot_iff, LieSubmodule.lcs_le_iff, hk k (le_refl k)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
⊢ H.normalizer = H
have hk' : LieSubmodule.ucs (k + 1) ⊥ = H.toLieSubmodule
Tactic: have hk' := hk (k + 1) k.le_succ
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
hk' : LieSubmodule.ucs (k + 1) ⊥ = H.toLieSubmodule
⊢ H.normalizer = H
have hk'₁ : H.toLieSubmodule.normalizer = H.toLieSubmodule
Tactic: rw [LieSubmodule.ucs_succ, hk k (le_refl k)] at hk'
Cleared hypotheses: hk'
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
hk' : H.toLieSubmodule.normalizer = H.toLieSubmodule
⊢ H.normalizer = H
have rw : H.normalizer.toSubmodule = H.toSubmodule
Tactic: rw [← LieSubalgebra.toSubmodule_inj, ← LieSubalgebra.coe_normalizer_eq_normalizer,
            hk', LieSubalgebra.coe_toLieSubmodule]