awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw : H.normalizer.toSubmodule = H.toSubmodule
⊢ H.normalizer = H
have rw₁ : (↑H.toLieSubmodule.normalizer : Submodule R L) = H.toSubmodule
Tactic: rw [← LieSubalgebra.toSubmodule_inj, ← LieSubalgebra.coe_normalizer_eq_normalizer,
            hk', LieSubalgebra.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
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
⊢ H.normalizer = H
have rw₂ : (↑H.toLieSubmodule : Submodule R L) = H.toSubmodule
Tactic: rw [← LieSubalgebra.toSubmodule_inj, ← LieSubalgebra.coe_normalizer_eq_normalizer,
            hk', LieSubalgebra.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
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
⊢ H.normalizer = H
have rw₃ : H.toSubmodule = H.toSubmodule
Tactic: rw [← LieSubalgebra.toSubmodule_inj, ← LieSubalgebra.coe_normalizer_eq_normalizer,
            hk', LieSubalgebra.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
inst_3 : Nontrivial L
H : LieSubalgebra R L
inst_4 : H.IsCartanSubalgebra
e : H = ⊥
⊢ False
have obtain : ∀ (x : L) (hx : x ≠ 0), False
Tactic: obtain ⟨x, hx⟩ := exists_ne (0 : L)
-- 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
inst_3 : Nontrivial L
H : LieSubalgebra R L
inst_4 : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
⊢ False
have this : x ∈ H.normalizer
Tactic: have : x ∈ H.normalizer := by simp [LieSubalgebra.mem_normalizer_iff, e]
-- 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
inst_3 : Nontrivial L
H : LieSubalgebra R L
inst_4 : H.IsCartanSubalgebra
e : H = ⊥
x : L
hx : x ≠ 0
this : x ∈ H.normalizer
⊢ x = 0
have rwa : ∀ (this : x ∈ H), x = 0
Tactic: rwa [LieSubalgebra.IsCartanSubalgebra.self_normalizing, e] at this
Cleared hypotheses: this
-- 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
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
⊢ x = 0
have rwa₁ : ∀ (this : Membership.mem (γ := LieSubalgebra R L) ⊥ x), x = 0
Tactic: rwa [LieSubalgebra.IsCartanSubalgebra.self_normalizing, e] at this
Cleared hypotheses: this
-- 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_1 : LieSubalgebra R L
inst_3 : Nontrivial L
H : LieSubalgebra R L
inst_4 : H.IsCartanSubalgebra
⊢ Nontrivial.{v} ↥H
have refine : ∀ (inst : Subsingleton.{v + 1} ↥H), False
Tactic: refine (subsingleton_or_nontrivial H).elim (fun inst ↦ False.elim ?_) id
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
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
⊢ False
have apply : H = ⊥
Tactic: apply ne_bot_of_isCartanSubalgebra H
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanSubalgebra (goal)
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
⊢ H = ⊥
have rw : ∀ x ∈ H, x = 0
Tactic: rw [eq_bot_iff]
-- 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
I : LieIdeal R L
⊢ (toLieSubalgebra R L I).normalizer = ⊤
have h : ∀ (x : L), x ∈ (toLieSubalgebra R L I).normalizer ↔ Membership.mem (γ := LieSubalgebra R L) ⊤ x
Tactic: ext x
-- 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 : LieRing.IsNilpotent L
⊢ Eq.{v + 1} (α := LieSubalgebra R L) (LieSubalgebra.normalizer ⊤) ⊤
have rw : Eq (α := LieSubalgebra R L) (LieSubalgebra.normalizer (toLieSubalgebra R L ⊤)) (toLieSubalgebra R L ⊤)
Tactic: rw [← top_toLieSubalgebra, normalizer_eq_top, top_toLieSubalgebra]
-- 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 : LieRing.IsNilpotent L
rw : Eq (α := LieSubalgebra R L) (LieSubalgebra.normalizer (toLieSubalgebra R L ⊤)) (toLieSubalgebra R L ⊤)
⊢ Eq.{v + 1} (α := LieSubalgebra R L) (LieSubalgebra.normalizer ⊤) ⊤
have rw₁ : Eq (α := LieSubalgebra R L) ⊤ (toLieSubalgebra R L ⊤)
Tactic: rw [← top_toLieSubalgebra, normalizer_eq_top, top_toLieSubalgebra]
-- 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 : LieRing.IsNilpotent L
rw : Eq (α := LieSubalgebra R L) (LieSubalgebra.normalizer (toLieSubalgebra R L ⊤)) (toLieSubalgebra R L ⊤)
rw₁ : Eq (α := LieSubalgebra R L) ⊤ (toLieSubalgebra R L ⊤)
⊢ Eq.{v + 1} (α := LieSubalgebra R L) (LieSubalgebra.normalizer ⊤) ⊤
have rw₂ : Eq.{v + 1} (α := LieSubalgebra R L) ⊤ ⊤
Tactic: rw [← top_toLieSubalgebra, normalizer_eq_top, top_toLieSubalgebra]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) ⁅x, y⁆ : R) (0 : R)
have rw : Eq.{u + 1} (α := R) (Bracket.bracket (L := R) ((χ : (a : L) → R) x : R) ((χ : (a : L) → R) y) : R) (0 : R)
Tactic: rw [LieHom.map_lie, LieRing.of_associative_ring_bracket, mul_comm, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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)
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) ⁅x, y⁆ : R) (0 : R)
have 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
Tactic: rw [LieHom.map_lie, LieRing.of_associative_ring_bracket, mul_comm, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) ⁅x, y⁆ : R) (0 : R)
have 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
Tactic: rw [LieHom.map_lie, LieRing.of_associative_ring_bracket, mul_comm, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) ⁅x, y⁆ : R) (0 : R)
have rw₃ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [LieHom.map_lie, LieRing.of_associative_ring_bracket, mul_comm, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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
⊢ Eq.{u + 1} (α := R) (Bracket.bracket (L := R) ((χ : (a : L) → R) x : R) ((χ : (a : L) → R) y) : R) (0 : R)
have 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
Tactic: rw [LieRing.of_associative_ring_bracket, mul_comm, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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
⊢ Eq.{u + 1} (α := R) (Bracket.bracket (L := R) ((χ : (a : L) → R) x : R) ((χ : (a : L) → R) y) : R) (0 : R)
have 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
Tactic: rw [LieRing.of_associative_ring_bracket, mul_comm, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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
⊢ Eq.{u + 1} (α := R) (Bracket.bracket (L := R) ((χ : (a : L) → R) x : R) ((χ : (a : L) → R) y) : R) (0 : R)
have rw₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [LieRing.of_associative_ring_bracket, mul_comm, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (hypothesis)
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
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) x : R) (0 : R)
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (hypothesis)
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
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) y : R) (0 : R)
have h₁ : ∃ (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) y : R) (0 : R)
have mem : ∀ (z w : L), Eq.{u + 1} (α := R) ((χ : (a : L) → R) ⁅z, w⁆ : R) (0 : R)
Tactic: obtain ⟨z, w, rfl⟩ := h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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)
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) (y + z) : R) (0 : R)
have add : HAdd.hAdd (α := R) (β := R) ((χ : (a : L) → R) y : R) ((χ : (a : L) → R) z : R) = 0
Tactic: rw [map_add, hy, hz, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) (y + z) : R) (0 : R)
have add₁ : HAdd.hAdd (α := R) (β := R) (0 : R) ((χ : (a : L) → R) z : R) = 0
Tactic: rw [map_add, hy, hz, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) (y + z) : R) (0 : R)
have add₂ : HAdd.hAdd (α := R) 0 0 = 0
Tactic: rw [map_add, hy, hz, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) (y + z) : R) (0 : R)
have add₃ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [map_add, hy, hz, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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)
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) (t • y) : R) (0 : R)
have smul : HSMul.hSMul (β := R) t ((χ : (a : L) → R) y : R) = 0
Tactic: rw [map_smul, hy, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) (t • y) : R) (0 : R)
have smul₁ : HSMul.hSMul (β := R) t 0 = 0
Tactic: rw [map_smul, hy, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) (t • y) : R) (0 : R)
have smul₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [map_smul, hy, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) x : R) (0 : R)
have 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)
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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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)
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) x : R) (0 : R)
have zero : Eq.{u + 1} (α := R) ((χ : (a : L) → R) 0 : 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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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)
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) x : R) (0 : R)
have 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)
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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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)
⊢ Eq.{u + 1} (α := R) ((χ : (a : L) → R) x : R) (0 : R)
have 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)
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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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
⊢ ψ.toFun ⁅x, y⁆ = ⁅ψ.toFun x, ψ.toFun y⁆
have rw : ψ.toFun 0 = ⁅ψ.toFun x, ψ.toFun y⁆
Tactic: rw [LieModule.IsTrivial.trivial, LieRing.of_associative_ring_bracket, mul_comm, sub_self,
          LinearMap.toFun_eq_coe, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Character (goal)
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⁆
⊢ ψ.toFun ⁅x, y⁆ = ⁅ψ.toFun x, ψ.toFun y⁆
have rw₁ : ψ.toFun 0 = ψ.toFun x * ψ.toFun y - ψ.toFun y * ψ.toFun x
Tactic: rw [LieModule.IsTrivial.trivial, LieRing.of_associative_ring_bracket, mul_comm, sub_self,
          LinearMap.toFun_eq_coe, map_zero]