awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
inst_5 : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' :
  ∀ (y : L'),
    Membership.mem (γ := LieIdeal R L') ⊤ y →
      Eq.{u_1 + 1} (α := R)
        ((((LieModule.traceForm R L' L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) y : R) (0 : R)
⊢ Membership.mem (γ := LieSubmodule R L' L') ⊥ x'
have killingCompl_top_eq_bot : Membership.mem (α := L) (γ := Submodule R L) (LinearMap.ker (killingForm R L)) ((e.symm : (a : L') → L) x' : L)
Tactic: suffices e.symm x' ∈ LinearMap.ker (killingForm R L) by
    rw [IsKilling.ker_killingForm_eq_bot] at this
    simpa [map_zero] using (e : L ≃ₗ[R] L').congr_arg this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
inst_5 : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' :
  ∀ (y : L'),
    Membership.mem (γ := LieIdeal R L') ⊤ y →
      Eq.{u_1 + 1} (α := R)
        ((((LieModule.traceForm R L' L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) y : R) (0 : R)
⊢ Membership.mem (α := L) (γ := Submodule R L) (LinearMap.ker (killingForm R L)) ((e.symm : (a : L') → L) x' : L)
have killingCompl_top_eq_bot : ∀ (y : L),
  Eq.{u_1 + 1} (α := R)
    ((((killingForm R L : (a : L) → L →ₗ[R] R) ((e.symm : (a : L') → L) x') : L →ₗ[R] R) : (a : L) → R) y : R)
    ((0 : (a : L) → R) y : R)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (hypothesis)
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
inst_5 : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' :
  ∀ (y : L'),
    Membership.mem (γ := LieIdeal R L') ⊤ y →
      Eq.{u_1 + 1} (α := R)
        ((((LieModule.traceForm R L' L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) y : R) (0 : R)
y : L
⊢ Eq.{u_1 + 1} (α := R)
    ((((killingForm R L : (a : L) → L →ₗ[R] R) ((e.symm : (a : L') → L) x') : L →ₗ[R] R) : (a : L) → R) y : R)
    ((0 : (a : L) → R) y : R)
have hx'₁ : ∀ (y' : L'),
  Eq.{u_1 + 1} (α := R) ((((killingForm R L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) y' : R) (0 : R)
Tactic: replace hx' : ∀ y', killingForm R L' x' y' = 0 := by simpa using hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (hypothesis)
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
inst_5 : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
y : L
hx' :
  ∀ (y' : L'),
    Eq.{u_1 + 1} (α := R) ((((killingForm R L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) y' : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((killingForm R L : (a : L) → L →ₗ[R] R) ((e.symm : (a : L') → L) x') : L →ₗ[R] R) : (a : L) → R) y : R)
    ((0 : (a : L) → R) y : R)
have hx'₁ : Eq.{u_1 + 1} (α := R)
  ((((killingForm R L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) ((e : (a : L) → L') y : L') : R)
  (0 : R)
Tactic: specialize hx' (e y)
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
inst_5 : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
y : L
hx' :
  Eq.{u_1 + 1} (α := R)
    ((((killingForm R L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) ((e : (a : L) → L') y : L') : R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((killingForm R L : (a : L) → L →ₗ[R] R) ((e.symm : (a : L') → L) x') : L →ₗ[R] R) : (a : L) → R) y : R)
    ((0 : (a : L) → R) y : R)
have killingCompl_top_eq_bot : ∀
  (hx' :
    Eq.{u_1 + 1} (α := R)
      ((((killingForm R L' : (a : L') → L' →ₗ[R] R) ((e : (a : L) → L') ((e.symm : (a : L') → L) x' : L)) :
              L' →ₗ[R] R) :
            (a : L') → R)
          ((e : (a : L) → L') y : L') :
        R)
      (0 : R)),
  Eq.{u_1 + 1} (α := R)
    ((((killingForm R L : (a : L) → L →ₗ[R] R) ((e.symm : (a : L') → L) x') : L →ₗ[R] R) : (a : L) → R) y : R)
    ((0 : (a : L) → R) y : R)
Tactic: rwa [← e.apply_symm_apply x', killingForm_of_equiv_apply] at hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
R : Type u_1
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : Type u_4
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
inst_5 : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
y : L
hx' :
  Eq.{u_1 + 1} (α := R)
    ((((killingForm R L' : (a : L') → L' →ₗ[R] R) x' : L' →ₗ[R] R) : (a : L') → R) ((e : (a : L) → L') y : L') : R)
    (0 : R)
killingCompl_top_eq_bot :
  ∀
    (hx' :
      Eq.{u_1 + 1} (α := R)
        ((((killingForm R L' : (a : L') → L' →ₗ[R] R) ((e : (a : L) → L') ((e.symm : (a : L') → L) x' : L)) :
                L' →ₗ[R] R) :
              (a : L') → R)
            ((e : (a : L) → L') y : L') :
          R)
        (0 : R)),
    Eq.{u_1 + 1} (α := R)
      ((((killingForm R L : (a : L) → L →ₗ[R] R) ((e.symm : (a : L') → L) x') : L →ₗ[R] R) : (a : L) → R) y : R)
      ((0 : (a : L) → R) y : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((killingForm R L : (a : L) → L →ₗ[R] R) ((e.symm : (a : L') → L) x') : L →ₗ[R] R) : (a : L) → R) y : R)
    ((0 : (a : L) → R) y : R)
have killingCompl_top_eq_bot₁ : ∀
  (hx' :
    Eq.{u_1 + 1} (α := R)
      ((((killingForm R L : (a : L) → L →ₗ[R] R) ((e.symm : (a : L') → L) x') : L →ₗ[R] R) : (a : L) → R) y : R)
      (0 : R)),
  Eq.{u_1 + 1} (α := R)
    ((((killingForm R L : (a : L) → L →ₗ[R] R) ((e.symm : (a : L') → L) x') : L →ₗ[R] R) : (a : L) → R) y : R)
    ((0 : (a : L) → R) y : R)
Tactic: rwa [← e.apply_symm_apply x', killingForm_of_equiv_apply] at hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
this : Disjoint I (killingCompl K L I)
⊢ IsCompl I (killingCompl K L I)
have rwa : IsCompl (↑I : Submodule K L) (↑(killingCompl K L I) : Submodule K L)
Tactic: rwa [← LieSubmodule.isCompl_toSubmodule, I.toSubmodule_killingCompl,
      LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint (LieModule.traceForm_isSymm K L L).isRefl,
      ← I.toSubmodule_killingCompl, LieSubmodule.disjoint_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
this : Disjoint I (killingCompl K L I)
rwa : IsCompl (↑I : Submodule K L) (↑(killingCompl K L I) : Submodule K L)
⊢ IsCompl I (killingCompl K L I)
have rwa₁ : IsCompl (↑I : Submodule K L) (LinearMap.BilinForm.orthogonal (killingForm K L) (↑I : Submodule K L))
Tactic: rwa [← LieSubmodule.isCompl_toSubmodule, I.toSubmodule_killingCompl,
      LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint (LieModule.traceForm_isSymm K L L).isRefl,
      ← I.toSubmodule_killingCompl, LieSubmodule.disjoint_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
this : Disjoint I (killingCompl K L I)
rwa : IsCompl (↑I : Submodule K L) (↑(killingCompl K L I) : Submodule K L)
rwa₁ : IsCompl (↑I : Submodule K L) (LinearMap.BilinForm.orthogonal (killingForm K L) (↑I : Submodule K L))
⊢ IsCompl I (killingCompl K L I)
have rwa₂ : Disjoint (↑I : Submodule K L) (LinearMap.BilinForm.orthogonal (LieModule.traceForm K L L) (↑I : Submodule K L))
Tactic: rwa [← LieSubmodule.isCompl_toSubmodule, I.toSubmodule_killingCompl,
      LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint (LieModule.traceForm_isSymm K L L).isRefl,
      ← I.toSubmodule_killingCompl, LieSubmodule.disjoint_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
this : Disjoint I (killingCompl K L I)
rwa : IsCompl (↑I : Submodule K L) (↑(killingCompl K L I) : Submodule K L)
rwa₁ : IsCompl (↑I : Submodule K L) (LinearMap.BilinForm.orthogonal (killingForm K L) (↑I : Submodule K L))
rwa₂ : Disjoint (↑I : Submodule K L) (LinearMap.BilinForm.orthogonal (LieModule.traceForm K L L) (↑I : Submodule K L))
⊢ IsCompl I (killingCompl K L I)
have rwa₃ : Disjoint (↑I : Submodule K L) (↑(killingCompl K L I) : Submodule K L)
Tactic: rwa [← LieSubmodule.isCompl_toSubmodule, I.toSubmodule_killingCompl,
      LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint (LieModule.traceForm_isSymm K L L).isRefl,
      ← I.toSubmodule_killingCompl, LieSubmodule.disjoint_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
⊢ IsCompl I (killingCompl K L I)
have suffices : Disjoint I (killingCompl K L I)
Tactic: suffices Disjoint I I.killingCompl by
    rwa [← LieSubmodule.isCompl_toSubmodule, I.toSubmodule_killingCompl,
      LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint (LieModule.traceForm_isSymm K L L).isRefl,
      ← I.toSubmodule_killingCompl, LieSubmodule.disjoint_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
this : IsLieAbelian.{u_3} ↥(I ⊓ killingCompl K L I)
⊢ Disjoint I (killingCompl K L I)
have rw : I ⊓ killingCompl K L I = ⊥
Tactic: rw [disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
⊢ Disjoint I (killingCompl K L I)
have suffices : IsLieAbelian.{u_3} ↥(I ⊓ killingCompl K L I)
Tactic: suffices IsLieAbelian (I ⊓ I.killingCompl : LieIdeal K L) by
    rw [disjoint_iff]
    exact IsKilling.ideal_eq_bot_of_isLieAbelian _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
this :
  ∀ (x y z : L) (hx : x ∈ killingCompl K L I) (hy : y ∈ I),
    Eq.{u_2 + 1} (α := K) ((((LieModule.traceForm K L L : (a : L) → L →ₗ[K] K) ⁅x, y⁆ : L →ₗ[K] K) : (a : L) → K) z : K)
      (0 : K)
⊢ IsLieAbelian.{u_3} ↥(I ⊓ killingCompl K L I)
have rw : ∀ x ∈ I ⊓ killingCompl K L I, ∀ m ∈ I ⊓ killingCompl K L I, ⁅x, m⁆ = 0
Tactic: rw [LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieSubmodule.lie_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
⊢ IsLieAbelian.{u_3} ↥(I ⊓ killingCompl K L I)
have suffices : ∀ (x y z : L) (hx : x ∈ killingCompl K L I) (hy : y ∈ I),
  Eq.{u_2 + 1} (α := K) ((((LieModule.traceForm K L L : (a : L) → L →ₗ[K] K) ⁅x, y⁆ : L →ₗ[K] K) : (a : L) → K) z : K)
    (0 : K)
Tactic: suffices ∀ (x y z : L) (hx : x ∈ killingCompl K L I) (hy : y ∈ I),
      LieModule.traceForm K L L ⁅x, y⁆ z = 0 by
    rw [LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieSubmodule.lie_eq_bot_iff]
    rintro x ⟨-, hx⟩ y ⟨hy, -⟩
    exact (IsKilling.killingForm_nondegenerate K L).1 _ fun z ↦ this x y z hx hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Killing (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : IsKilling K L
inst_4 : Module.Finite K L
I : LieIdeal K L
x y z : L
hx : x ∈ killingCompl K L I
hy : y ∈ I
⊢ Eq.{u_2 + 1} (α := K) ((((LieModule.traceForm K L L : (a : L) → L →ₗ[K] K) ⁅x, y⁆ : L →ₗ[K] K) : (a : L) → K) z : K)
    (0 : K)
have rw : Eq.{u_2 + 1} (α := K) ((((LieModule.traceForm K L L : (a : L) → L →ₗ[K] K) ⁅y, z⁆ : L →ₗ[K] K) : (a : L) → K) x : K)
  (0 : K)
Tactic: rw [LieModule.traceForm_apply_lie_apply K L L x y z, LieModule.traceForm_comm K L L]
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : Membership.mem (γ := LieSubmodule R A V) (weightSpace V χ) v
⊢ Membership.mem (γ := LieSubmodule R A V) (weightSpace V χ) ⁅z, v⁆
have rw : ∀ (hv : ∀ (x : A), ⁅x, v⁆ = χ x • v) (x : A), ⁅x, ⁅z, v⁆⁆ = χ x • ⁅z, v⁆
Tactic: rw [mem_weightSpace] at hv ⊢
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
⊢ ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆
have inl : ∀ (hv : ∀ (x : A), ⁅x, 0⁆ = HSMul.hSMul (β := V) (χ x) 0), ⁅a, ⁅z, 0⁆⁆ = HSMul.hSMul (β := V) (χ a) ⁅z, 0⁆
Tactic: rcases eq_or_ne v 0 with (rfl | hv')
Cleared hypotheses: v, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
inl : ∀ (hv : ∀ (x : A), ⁅x, 0⁆ = HSMul.hSMul (β := V) (χ x) 0), ⁅a, ⁅z, 0⁆⁆ = HSMul.hSMul (β := V) (χ a) ⁅z, 0⁆
⊢ ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆
have inr : ∀ (hv' : v ≠ 0), ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆
Tactic: rcases eq_or_ne v 0 with (rfl | hv')
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
this : χ ⁅z, a⁆ = 0
⊢ ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆
have rw : ⁅⁅a, z⁆, v⁆ + ⁅z, ⁅a, v⁆⁆ = χ a • ⁅z, v⁆
Tactic: rw [leibniz_lie, hv a, lie_smul, lie_swap_lie, hv, this, zero_smul, neg_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
this : χ ⁅z, a⁆ = 0
rw : ⁅⁅a, z⁆, v⁆ + ⁅z, ⁅a, v⁆⁆ = χ a • ⁅z, v⁆
⊢ ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆
have rw₁ : ⁅⁅a, z⁆, v⁆ + ⁅z, χ a • v⁆ = χ a • ⁅z, v⁆
Tactic: rw [leibniz_lie, hv a, lie_smul, lie_swap_lie, hv, this, zero_smul, neg_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
this : χ ⁅z, a⁆ = 0
rw : ⁅⁅a, z⁆, v⁆ + ⁅z, ⁅a, v⁆⁆ = χ a • ⁅z, v⁆
rw₁ : ⁅⁅a, z⁆, v⁆ + ⁅z, χ a • v⁆ = χ a • ⁅z, v⁆
⊢ ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆
have rw₂ : ⁅⁅a, z⁆, v⁆ + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
Tactic: rw [leibniz_lie, hv a, lie_smul, lie_swap_lie, hv, this, zero_smul, neg_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
this : χ ⁅z, a⁆ = 0
rw : ⁅⁅a, z⁆, v⁆ + ⁅z, ⁅a, v⁆⁆ = χ a • ⁅z, v⁆
rw₁ : ⁅⁅a, z⁆, v⁆ + ⁅z, χ a • v⁆ = χ a • ⁅z, v⁆
rw₂ : ⁅⁅a, z⁆, v⁆ + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
⊢ ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆
have rw₃ : -⁅⁅z, a⁆, v⁆ + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
Tactic: rw [leibniz_lie, hv a, lie_smul, lie_swap_lie, hv, this, zero_smul, neg_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
this : χ ⁅z, a⁆ = 0
rw : ⁅⁅a, z⁆, v⁆ + ⁅z, ⁅a, v⁆⁆ = χ a • ⁅z, v⁆
rw₁ : ⁅⁅a, z⁆, v⁆ + ⁅z, χ a • v⁆ = χ a • ⁅z, v⁆
rw₂ : ⁅⁅a, z⁆, v⁆ + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₃ : -⁅⁅z, a⁆, v⁆ + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
⊢ ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆
have rw₄ : -(χ ⁅z, a⁆ • v) + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
Tactic: rw [leibniz_lie, hv a, lie_smul, lie_swap_lie, hv, this, zero_smul, neg_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
this : χ ⁅z, a⁆ = 0
rw : ⁅⁅a, z⁆, v⁆ + ⁅z, ⁅a, v⁆⁆ = χ a • ⁅z, v⁆
rw₁ : ⁅⁅a, z⁆, v⁆ + ⁅z, χ a • v⁆ = χ a • ⁅z, v⁆
rw₂ : ⁅⁅a, z⁆, v⁆ + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₃ : -⁅⁅z, a⁆, v⁆ + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₄ : -(χ ⁅z, a⁆ • v) + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
⊢ ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆
have rw₅ : -HSMul.hSMul.{u_1, u_4, u_4} (α := R) 0 v + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
Tactic: rw [leibniz_lie, hv a, lie_smul, lie_swap_lie, hv, this, zero_smul, neg_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
this : χ ⁅z, a⁆ = 0
rw : ⁅⁅a, z⁆, v⁆ + ⁅z, ⁅a, v⁆⁆ = χ a • ⁅z, v⁆
rw₁ : ⁅⁅a, z⁆, v⁆ + ⁅z, χ a • v⁆ = χ a • ⁅z, v⁆
rw₂ : ⁅⁅a, z⁆, v⁆ + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₃ : -⁅⁅z, a⁆, v⁆ + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₄ : -(χ ⁅z, a⁆ • v) + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₅ : -HSMul.hSMul.{u_1, u_4, u_4} (α := R) 0 v + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
⊢ ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆
have rw₆ : -0 + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
Tactic: rw [leibniz_lie, hv a, lie_smul, lie_swap_lie, hv, this, zero_smul, neg_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.LieTheorem (goal)
Goal:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : LieRing L
inst_5 : LieAlgebra R L
inst_6 : LieRing A
inst_7 : LieAlgebra R A
inst_8 : Bracket L A
inst_9 : Bracket A L
inst_10 : AddCommGroup V
inst_11 : Module R V
inst_12 : Module.Free R V
inst_13 : Module.Finite R V
inst_14 : LieRingModule L V
inst_15 : LieModule R L V
inst_16 : LieRingModule A V
inst_17 : LieModule R A V
inst_18 : IsLieTower L A V
inst_19 : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
this : χ ⁅z, a⁆ = 0
rw : ⁅⁅a, z⁆, v⁆ + ⁅z, ⁅a, v⁆⁆ = χ a • ⁅z, v⁆
rw₁ : ⁅⁅a, z⁆, v⁆ + ⁅z, χ a • v⁆ = χ a • ⁅z, v⁆
rw₂ : ⁅⁅a, z⁆, v⁆ + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₃ : -⁅⁅z, a⁆, v⁆ + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₄ : -(χ ⁅z, a⁆ • v) + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₅ : -HSMul.hSMul.{u_1, u_4, u_4} (α := R) 0 v + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
rw₆ : -0 + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
⊢ ⁅a, ⁅z, v⁆⁆ = χ a • ⁅z, v⁆
have rw₇ : 0 + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
Tactic: rw [leibniz_lie, hv a, lie_smul, lie_swap_lie, hv, this, zero_smul, neg_zero, zero_add]