awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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
succ :
  ∀ (k : ℕ) (ih : LieSubmodule.ucs k H.toLieSubmodule = H.toLieSubmodule),
    LieSubmodule.ucs (k + 1) H.toLieSubmodule = H.toLieSubmodule
⊢ LieSubmodule.ucs k H.toLieSubmodule = H.toLieSubmodule

Tactic:
induction k with
  | zero => simp
  | succ k ih => simp [ih]
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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
mpr : H.toLieSubmodule.IsUcsLimit → H.IsCartanSubalgebra
⊢ H.IsCartanSubalgebra ↔ H.toLieSubmodule.IsUcsLimit

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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
⊢ LieRing.IsNilpotent.{v} ↥H

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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
⊢ LieRing.IsNilpotent.{v} ↥H

Tactic:
have h₁ : LieRing.IsNilpotent H := by infer_instance
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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
mp : ∀ (k : ℕ) (hk : H.toLieSubmodule ≤ LieSubmodule.ucs k ⊥), H.toLieSubmodule.IsUcsLimit
⊢ H.toLieSubmodule.IsUcsLimit

Tactic:
obtain ⟨k, hk⟩ := H.toLieSubmodule.isNilpotent_iff_exists_self_le_ucs.mp h₁

Premises used: LieSubmodule.isNilpotent_iff_exists_self_le_ucs, LieSubalgebra.toLieSubmodule, Iff.mp
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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 = 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)
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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

Tactic:
⟨k, fun l hl => ?_⟩

Premises used: LieSubmodule.IsUcsLimit, Exists.intro
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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 ⊥
mp : ∀ (l : ℕ) (hl : k ≤ l), LieSubmodule.ucs l ⊥ = H.toLieSubmodule
⊢ H.toLieSubmodule.IsUcsLimit

Tactic:
refine ⟨k, fun l hl => ?_⟩
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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
mp₃ mp₄ : H.toLieSubmodule = H.toLieSubmodule
⊢ LieSubmodule.ucs l ⊥ = H.toLieSubmodule

Tactic:
rw [← Nat.sub_add_cancel hl, LieSubmodule.ucs_add, ← hk,
      LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra]

Premises used: LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra, Nat.sub_add_cancel, LieSubmodule.ucs_add
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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
erw : ∃ (k : ℕ), LieSubmodule.lcs k H.toLieSubmodule = ⊥
⊢ LieModule.IsNilpotent.{v, v} ↥H ↥H

Tactic:
erw [H.toLieSubmodule.isNilpotent_iff_exists_lcs_eq_bot]

Premises used: LieSubmodule.isNilpotent_iff_exists_lcs_eq_bot, LieSubalgebra.toLieSubmodule
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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 = ⊥
⊢ ∃ (k : ℕ), LieSubmodule.lcs k H.toLieSubmodule = ⊥

Tactic:
use k
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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 ⊥
h₂ h₃ : H.toLieSubmodule ≤ H.toLieSubmodule
⊢ LieSubmodule.lcs k H.toLieSubmodule = ⊥

Tactic:
rw [_root_.eq_bot_iff, LieSubmodule.lcs_le_iff, hk k (le_refl k)]

Premises used: le_refl, LieSubmodule.lcs_le_iff, eq_bot_iff
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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.ucs (k + 1) ⊥ = H.toLieSubmodule

Tactic:
have hk' := hk (k + 1) k.le_succ
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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.toLieSubmodule.normalizer = H.toLieSubmodule

Tactic:
rw [LieSubmodule.ucs_succ, hk k (le_refl k)] at hk'

Premises used: le_refl, LieSubmodule.ucs_succ
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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
rw : H.normalizer.toSubmodule = H.toSubmodule
rw₁ : (↑H.toLieSubmodule.normalizer : Submodule R L) = H.toSubmodule
rw₂ : (↑H.toLieSubmodule : Submodule R L) = H.toSubmodule
rw₃ rw₄ : H.toSubmodule = H.toSubmodule
⊢ H.normalizer = H

Tactic:
rw [← LieSubalgebra.toSubmodule_inj, ← LieSubalgebra.coe_normalizer_eq_normalizer,
            hk', LieSubalgebra.coe_toLieSubmodule]

Premises used: LieSubalgebra.coe_normalizer_eq_normalizer, LieSubalgebra.toSubmodule_inj, LieSubalgebra.coe_toLieSubmodule
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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.IsCartanSubalgebra

Tactic:
exact
      { nilpotent := by
          dsimp only [LieRing.IsNilpotent]
          -- The instance for the second `H` in the goal is `lieRingSelfModule`
          -- but `rw` expects it to be `H.toLieSubmodule.instLieRingModuleSubtypeMem`,
          -- and these are not reducibly defeq.
          erw [H.toLieSubmodule.isNilpotent_iff_exists_lcs_eq_bot]
          use k
          rw [_root_.eq_bot_iff, LieSubmodule.lcs_le_iff, hk k (le_refl k)]
        self_normalizing := by
          have hk' := hk (k + 1) k.le_succ
          rw [LieSubmodule.ucs_succ, hk k (le_refl k)] at hk'
          rw [← LieSubalgebra.toSubmodule_inj, ← LieSubalgebra.coe_normalizer_eq_normalizer,
            hk', LieSubalgebra.coe_toLieSubmodule] }
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Nontrivial L
H : LieSubalgebra R L
inst_4 : H.IsCartanSubalgebra
e : H = ⊥
obtain : ∀ (x : L) (hx : x ≠ 0), False
⊢ False

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : L)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Nontrivial L
H : LieSubalgebra R L
inst_4 : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
⊢ x ∈ H.normalizer

Tactic:
simp [LieSubalgebra.mem_normalizer_iff, e]

Premises used: LieSubalgebra.mem_normalizer_iff
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Nontrivial L
H : LieSubalgebra R L
inst_4 : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
⊢ x ∈ H.normalizer

Tactic:
have : x ∈ H.normalizer := by simp [LieSubalgebra.mem_normalizer_iff, e]
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Nontrivial L
H : LieSubalgebra R L
inst_4 : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
this : x ∈ H.normalizer
rwa : ∀ (this : x ∈ H), x = 0
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : Membership.mem (γ := LieSubalgebra R L) ⊥ x), x = 0
⊢ x = 0

Tactic:
rwa [LieSubalgebra.IsCartanSubalgebra.self_normalizing, e] at this

Premises used: LieSubalgebra.IsCartanSubalgebra.self_normalizing
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Nontrivial L
H : LieSubalgebra R L
inst_4 : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
this : x ∈ H.normalizer
⊢ False

Tactic:
exact hx (by rwa [LieSubalgebra.IsCartanSubalgebra.self_normalizing, e] at this)
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H_1 : LieSubalgebra R L
inst_3 : Nontrivial L
H : LieSubalgebra R L
inst_4 : H.IsCartanSubalgebra
⊢ Nontrivial.{v} ↥H

Tactic:
(subsingleton_or_nontrivial H).elim (fun inst ↦ False.elim ?_) id

Premises used: False.elim, Membership.mem, id, Subtype, subsingleton_or_nontrivial, Or.elim
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H_1 : LieSubalgebra R L
inst_3 : Nontrivial L
H : LieSubalgebra R L
inst_4 : H.IsCartanSubalgebra
refine : ∀ (inst : Subsingleton.{v + 1} ↥H), False
⊢ Nontrivial.{v} ↥H

Tactic:
refine (subsingleton_or_nontrivial H).elim (fun inst ↦ False.elim ?_) id

Premises used: False.elim, Membership.mem, id, Subtype, subsingleton_or_nontrivial, Or.elim
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
H_1 : LieSubalgebra R L
inst_4 : Nontrivial L
H : LieSubalgebra R L
inst_5 : H.IsCartanSubalgebra
inst : Subsingleton.{v + 1} ↥H
apply : H = ⊥
⊢ False

Tactic:
apply ne_bot_of_isCartanSubalgebra H

Premises used: LieSubalgebra.ne_bot_of_isCartanSubalgebra
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
H_1 : LieSubalgebra R L
inst_4 : Nontrivial L
H : LieSubalgebra R L
inst_5 : H.IsCartanSubalgebra
inst : Subsingleton.{v + 1} ↥H
rw : ∀ x ∈ H, x = 0
⊢ H = ⊥

Tactic:
rw [eq_bot_iff]

Premises used: LieSubalgebra.eq_bot_iff
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
H_1 : LieSubalgebra R L
inst_4 : Nontrivial L
H : LieSubalgebra R L
inst_5 : H.IsCartanSubalgebra
inst : Subsingleton.{v + 1} ↥H
⊢ ∀ x ∈ H, x = 0

Tactic:
fun x hx ↦ congr_arg Subtype.val (Subsingleton.elim (⟨x, hx⟩ : H) 0)

Premises used: Subtype.mk, congr_arg, Subsingleton.elim, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
H_1 : LieSubalgebra R L
inst_4 : Nontrivial L
H : LieSubalgebra R L
inst_5 : H.IsCartanSubalgebra
inst : Subsingleton.{v + 1} ↥H
⊢ ∀ x ∈ H, x = 0

Tactic:
exact fun x hx ↦ congr_arg Subtype.val (Subsingleton.elim (⟨x, hx⟩ : H) 0)

Premises used: Subtype.mk, congr_arg, Subsingleton.elim, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h : ∀ (x : L), x ∈ (toLieSubalgebra R L I).normalizer ↔ Membership.mem (γ := LieSubalgebra R L) ⊤ x
⊢ (toLieSubalgebra R L I).normalizer = ⊤

Tactic:
ext x
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x : L
⊢ x ∈ (toLieSubalgebra R L I).normalizer ↔ Membership.mem (γ := LieSubalgebra R L) ⊤ x

Tactic:
simpa only [LieSubalgebra.mem_normalizer_iff, LieSubalgebra.mem_top, iff_true] using
    fun y hy => I.lie_mem hy

Premises used: iff_true, LieSubmodule.lie_mem, LieSubalgebra.mem_top, LieSubalgebra.mem_normalizer_iff
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
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 : LieRing.IsNilpotent L
rw : Eq (α := LieSubalgebra R L) (LieSubalgebra.normalizer (toLieSubalgebra R L ⊤)) (toLieSubalgebra R L ⊤)
rw₁ : Eq (α := LieSubalgebra R L) ⊤ (toLieSubalgebra R L ⊤)
rw₂ rw₃ : Eq.{v + 1} (α := LieSubalgebra R L) ⊤ ⊤
⊢ Eq.{v + 1} (α := LieSubalgebra R L) (LieSubalgebra.normalizer ⊤) ⊤

Tactic:
rw [← top_toLieSubalgebra, normalizer_eq_top, top_toLieSubalgebra]

Premises used: LieIdeal.normalizer_eq_top, LieIdeal.top_toLieSubalgebra
-- Module: Mathlib.Algebra.Lie.Character
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
χ : LieCharacter R L
x y : L
rw : Eq.{u + 1} (α := R) (Bracket.bracket (L := R) ((χ : (a : L) → R) x : R) ((χ : (a : L) → R) y) : R) (0 : R)
rw₁ :
  HMul.hMul (α := R) (β := R) ((χ : (a : L) → R) x : R) ((χ : (a : L) → R) y : R) -
      HMul.hMul (α := R) (β := R) ((χ : (a : L) → R) y : R) ((χ : (a : L) → R) x : R) =
    0
rw₂ :
  HMul.hMul (α := R) (β := R) ((χ : (a : L) → R) y : R) ((χ : (a : L) → R) x : R) -
      HMul.hMul (α := R) (β := R) ((χ : (a : L) → R) y : R) ((χ : (a : L) → R) x : R) =
    0
rw₃ rw₄ : Eq.{u + 1} (α := R) 0 0
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) ⁅x, y⁆ : R) (0 : R)

Tactic:
rw [LieHom.map_lie, LieRing.of_associative_ring_bracket, mul_comm, sub_self]

Premises used: sub_self, LieHom.map_lie, LieRing.of_associative_ring_bracket, mul_comm
-- Module: Mathlib.Algebra.Lie.Character
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
χ : LieCharacter R L
x y : L
rw :
  HMul.hMul (α := R) (β := R) ((χ : (a : L) → R) x : R) ((χ : (a : L) → R) y : R) -
      HMul.hMul (α := R) (β := R) ((χ : (a : L) → R) y : R) ((χ : (a : L) → R) x : R) =
    0
rw₁ :
  HMul.hMul (α := R) (β := R) ((χ : (a : L) → R) y : R) ((χ : (a : L) → R) x : R) -
      HMul.hMul (α := R) (β := R) ((χ : (a : L) → R) y : R) ((χ : (a : L) → R) x : R) =
    0
rw₂ rw₃ : Eq.{u + 1} (α := R) 0 0
⊢ Eq.{u + 1} (α := R) (Bracket.bracket (L := R) ((χ : (a : L) → R) x : R) ((χ : (a : L) → R) y) : R) (0 : R)

Tactic:
rw [LieRing.of_associative_ring_bracket, mul_comm, sub_self]

Premises used: sub_self, LieRing.of_associative_ring_bracket, mul_comm
-- Module: Mathlib.Algebra.Lie.Character
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
χ : LieCharacter R L
x : L
h : Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) x
⊢ Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (x_1 : ↥⊤) (n : ↥⊤), ⁅(↑x_1 : L), (↑n : L)⁆ = x}) x

Tactic:
rw [derivedSeries_def, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero, ←
    LieSubmodule.mem_toSubmodule, LieSubmodule.lieIdeal_oper_eq_linear_span] at h

Premises used: LieSubmodule.mem_toSubmodule, LieAlgebra.derivedSeriesOfIdeal_succ, LieAlgebra.derivedSeries_def, LieSubmodule.lieIdeal_oper_eq_linear_span, LieAlgebra.derivedSeriesOfIdeal_zero
-- Module: Mathlib.Algebra.Lie.Character
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
χ : LieCharacter R L
x y : L
h : Membership.mem (γ := Set L) {x : L | ∃ (x_1 : ↥⊤) (n : ↥⊤), ⁅(↑x_1 : L), (↑n : L)⁆ = x} y
⊢ ∃ (a : L) (a_1 : L), ⁅a, a_1⁆ = y

Tactic:
simp only [Subtype.exists, LieSubmodule.mem_top, exists_const, Set.mem_setOf_eq] at h

Premises used: Subtype.exists, Set.mem_setOf_eq, exists_const, LieSubmodule.mem_top
-- Module: Mathlib.Algebra.Lie.Character
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
χ : LieCharacter R L
x y : L
h : ∃ (a : L) (a_1 : L), ⁅a, a_1⁆ = y
mem : ∀ (z w : L), Eq.{u + 1} (α := R) ((χ : (a : L) → R) ⁅z, w⁆ : R) (0 : R)
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) y : R) (0 : R)

Tactic:
obtain ⟨z, w, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Character
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
χ : LieCharacter R L
x z w : L
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) ⁅z, w⁆ : R) (0 : R)

Tactic:
lieCharacter_apply_lie ..

Premises used: LieAlgebra.lieCharacter_apply_lie
-- Module: Mathlib.Algebra.Lie.Character
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
χ : LieCharacter R L
x z w : L
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) ⁅z, w⁆ : R) (0 : R)

Tactic:
exact lieCharacter_apply_lie ..

Premises used: LieAlgebra.lieCharacter_apply_lie
-- Module: Mathlib.Algebra.Lie.Character
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
χ : LieCharacter R L
x : L
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) 0 : R) (0 : R)

Tactic:
map_zero _

Premises used: map_zero
-- Module: Mathlib.Algebra.Lie.Character
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
χ : LieCharacter R L
x : L
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) 0 : R) (0 : R)

Tactic:
exact map_zero _

Premises used: map_zero
-- Module: Mathlib.Algebra.Lie.Character
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
χ : LieCharacter R L
x y z : L
hx :
  Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (x_1 : ↥⊤) (n : ↥⊤), ⁅(↑x_1 : L), (↑n : L)⁆ = x}) y
hy_1 :
  Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (x_1 : ↥⊤) (n : ↥⊤), ⁅(↑x_1 : L), (↑n : L)⁆ = x}) z
hy : Eq.{u + 1} (α := R) ((χ : (a : L) → R) y : R) (0 : R)
hz : Eq.{u + 1} (α := R) ((χ : (a : L) → R) z : R) (0 : R)
add : HAdd.hAdd (α := R) (β := R) ((χ : (a : L) → R) y : R) ((χ : (a : L) → R) z : R) = 0
add₁ : HAdd.hAdd (α := R) (β := R) (0 : R) ((χ : (a : L) → R) z : R) = 0
add₂ : HAdd.hAdd (α := R) 0 0 = 0
add₃ add₄ : Eq.{u + 1} (α := R) 0 0
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) (y + z) : R) (0 : R)

Tactic:
rw [map_add, hy, hz, add_zero]

Premises used: map_add, add_zero
-- Module: Mathlib.Algebra.Lie.Character
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
χ : LieCharacter R L
x : L
t : R
y : L
hx :
  Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (x_1 : ↥⊤) (n : ↥⊤), ⁅(↑x_1 : L), (↑n : L)⁆ = x}) y
hy : Eq.{u + 1} (α := R) ((χ : (a : L) → R) y : R) (0 : R)
smul : HSMul.hSMul (β := R) t ((χ : (a : L) → R) y : R) = 0
smul₁ : HSMul.hSMul (β := R) t 0 = 0
smul₂ smul₃ : Eq.{u + 1} (α := R) 0 0
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) (t • y) : R) (0 : R)

Tactic:
rw [map_smul, hy, smul_zero]

Premises used: smul_zero, map_smul
-- Module: Mathlib.Algebra.Lie.Character
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
χ : LieCharacter R L
x : L
h : Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (x_1 : ↥⊤) (n : ↥⊤), ⁅(↑x_1 : L), (↑n : L)⁆ = x}) x
mem :
  ∀ (y : L) (h : Membership.mem (γ := Set L) {x : L | ∃ (x_1 : ↥⊤) (n : ↥⊤), ⁅(↑x_1 : L), (↑n : L)⁆ = x} y),
    Eq.{u + 1} (α := R) ((χ : (a : L) → R) y : R) (0 : R)
zero : Eq.{u + 1} (α := R) ((χ : (a : L) → R) 0 : R) (0 : R)
add :
  ∀ (y z : L),
    Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (x_1 : ↥⊤) (n : ↥⊤), ⁅(↑x_1 : L), (↑n : L)⁆ = x})
        y →
      Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (x_1 : ↥⊤) (n : ↥⊤), ⁅(↑x_1 : L), (↑n : L)⁆ = x})
          z →
        ∀ (hy : Eq.{u + 1} (α := R) ((χ : (a : L) → R) y : R) (0 : R))
          (hz : Eq.{u + 1} (α := R) ((χ : (a : L) → R) z : R) (0 : R)),
          Eq.{u + 1} (α := R) ((χ : (a : L) → R) (y + z) : R) (0 : R)
smul :
  ∀ (t : R) (y : L),
    Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (x_1 : ↥⊤) (n : ↥⊤), ⁅(↑x_1 : L), (↑n : L)⁆ = x})
        y →
      ∀ (hy : Eq.{u + 1} (α := R) ((χ : (a : L) → R) y : R) (0 : R)),
        Eq.{u + 1} (α := R) ((χ : (a : L) → R) (t • y) : R) (0 : R)
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) x : R) (0 : R)

Tactic:
induction h using Submodule.span_induction with
  | mem y h =>
    simp only [Subtype.exists, LieSubmodule.mem_top, exists_const, Set.mem_setOf_eq] at h
    obtain ⟨z, w, rfl⟩ := h
    exact lieCharacter_apply_lie ..
  | zero => exact map_zero _
  | add y z _ _ hy hz => rw [map_add, hy, hz, add_zero]
  | smul t y _ hy => rw [map_smul, hy, smul_zero]

Premises used: smul_zero, Subtype.exists, map_zero, map_add, Set.mem_setOf_eq, exists_const, LieSubmodule.mem_top, LieAlgebra.lieCharacter_apply_lie, add_zero, rfl, map_smul
-- Module: Mathlib.Algebra.Lie.Character
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsLieAbelian L
ψ : Module.Dual R L
x y : L
rw : ψ.toFun 0 = ⁅ψ.toFun x, ψ.toFun y⁆
rw₁ : ψ.toFun 0 = ψ.toFun x * ψ.toFun y - ψ.toFun y * ψ.toFun x
rw₂ : ψ.toFun 0 = ψ.toFun y * ψ.toFun x - ψ.toFun y * ψ.toFun x
rw₃ : ψ.toFun 0 = 0
rw₄ : Eq.{u + 1} (α := R) ((ψ : (a : L) → R) 0 : R) (0 : R)
rw₅ rw₆ : Eq.{u + 1} (α := R) 0 0
⊢ ψ.toFun ⁅x, y⁆ = ⁅ψ.toFun x, ψ.toFun y⁆

Tactic:
rw [LieModule.IsTrivial.trivial, LieRing.of_associative_ring_bracket, mul_comm, sub_self,
          LinearMap.toFun_eq_coe, map_zero]

Premises used: sub_self, LinearMap.toFun_eq_coe, map_zero, LieRing.of_associative_ring_bracket, mul_comm, LieModule.IsTrivial.trivial
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
X Y : Matrix n n R
⊢ ⁅X, Y⁆.trace = 0

Tactic:
calc
    _ = Matrix.trace (X * Y) - Matrix.trace (Y * X) := trace_sub _ _
    _ = Matrix.trace (X * Y) - Matrix.trace (X * Y) :=
      (congr_arg (fun x => _ - x) (Matrix.trace_mul_comm Y X))
    _ = 0 := sub_self _

Premises used: Trans.trans, sub_self, Matrix.trace_mul_comm, HSub.hSub, congr_arg, Matrix.trace_sub
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
A B : ↥(sl n R)
⊢ (↑⁅A, B⁆ : Matrix n n R) = (↑A : Matrix n n R) * (↑B : Matrix n n R) - (↑B : Matrix n n R) * (↑A : Matrix n n R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
i j : n
h : i ≠ j
r : R
⊢ (↑((single i j h : (a : R) → ↥(sl n R)) r) : Matrix n n R) = Matrix.single i j r

Tactic:
rfl

Premises used: rfl, Matrix.single
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : DecidableEq q
inst_3 : DecidableEq l
inst_4 : CommRing R
inst_5 : Fintype n
i j k : n
r : R
⊢ Eq.{u₂ + 1} (α := R)
    ((traceLinearMap n R R : (a : Matrix n n R) → R)
        ((singleLinearMap R i i : (a : R) → Matrix n n R) r : Matrix n n R) :
      R)
    ((traceLinearMap n R R : (a : Matrix n n R) → R)
        ((singleLinearMap R j j : (a : R) → Matrix n n R) r : Matrix n n R) :
      R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Classical
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
i j : n
r : R
⊢ (↑((singleSubSingle i j : (a : R) → ↥(sl n R)) r) : Matrix n n R) = Matrix.single i i r - Matrix.single j j r

Tactic:
rfl

Premises used: rfl, Matrix.single