awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
x : M ≃ₗ⁅R,L⁆ N
x_1 : R
x_2 : M
⊢ (x : (a : M) → N) (x_1 • x_2) =
    HSMul.hSMul (α := R) (β := N) ((RingHom.id R : (a : R) → R) x_1 : R) ((x : (a : M) → N) x_2 : N)
have rw : (x.toLinearEquiv : (a : M) → N) (x_1 • x_2) =
  HSMul.hSMul (α := R) (β := N) ((RingHom.id R : (a : R) → R) x_1 : R) ((x.toLinearEquiv : (a : M) → N) x_2 : N)
Tactic: rw [← coe_toLinearEquiv, map_smul, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
x : M ≃ₗ⁅R,L⁆ N
x_1 : R
x_2 : M
rw :
  (x.toLinearEquiv : (a : M) → N) (x_1 • x_2) =
    HSMul.hSMul (α := R) (β := N) ((RingHom.id R : (a : R) → R) x_1 : R) ((x.toLinearEquiv : (a : M) → N) x_2 : N)
⊢ (x : (a : M) → N) (x_1 • x_2) =
    HSMul.hSMul (α := R) (β := N) ((RingHom.id R : (a : R) → R) x_1 : R) ((x : (a : M) → N) x_2 : N)
have rw₁ : HSMul.hSMul (β := N) x_1 ((x.toLinearEquiv : (a : M) → N) x_2 : N) =
  HSMul.hSMul (α := R) (β := N) ((RingHom.id R : (a : R) → R) x_1 : R) ((x.toLinearEquiv : (a : M) → N) x_2 : N)
Tactic: rw [← coe_toLinearEquiv, map_smul, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
x : M ≃ₗ⁅R,L⁆ N
x_1 : R
x_2 : M
rw :
  (x.toLinearEquiv : (a : M) → N) (x_1 • x_2) =
    HSMul.hSMul (α := R) (β := N) ((RingHom.id R : (a : R) → R) x_1 : R) ((x.toLinearEquiv : (a : M) → N) x_2 : N)
rw₁ :
  HSMul.hSMul (β := N) x_1 ((x.toLinearEquiv : (a : M) → N) x_2 : N) =
    HSMul.hSMul (α := R) (β := N) ((RingHom.id R : (a : R) → R) x_1 : R) ((x.toLinearEquiv : (a : M) → N) x_2 : N)
⊢ (x : (a : M) → N) (x_1 • x_2) =
    HSMul.hSMul (α := R) (β := N) ((RingHom.id R : (a : R) → R) x_1 : R) ((x : (a : M) → N) x_2 : N)
have rw₂ : HSMul.hSMul (β := N) x_1 ((x.toLinearEquiv : (a : M) → N) x_2 : N) =
  HSMul.hSMul (β := N) x_1 ((x.toLinearEquiv : (a : M) → N) x_2 : N)
Tactic: rw [← coe_toLinearEquiv, map_smul, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : IsAddTorsionFree L
i : ι
⊢ b.A i i = 2
have this : NoZeroSMulDivisors ℤ L
Tactic: have : NoZeroSMulDivisors ℤ L := IsAddTorsionFree.to_noZeroSMulDivisors_int
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : IsAddTorsionFree L
i : ι
this : NoZeroSMulDivisors ℤ L
⊢ (b.A i i - 2) • b.e i = 0
have rw : b.A i i • b.e i - b.A i i • b.e i = 0
Tactic: rw [sub_smul, ofNat_smul_eq_nsmul, ← (b.sl2 i).lie_h_e_nsmul, b.lie_h_e i i]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : IsAddTorsionFree L
i : ι
this : NoZeroSMulDivisors ℤ L
⊢ b.A i i = 2
have aux : (b.A i i - 2) • b.e i = 0
Tactic: have aux : (b.A i i - 2) • b.e i = 0 := by
    rw [sub_smul, ofNat_smul_eq_nsmul, ← (b.sl2 i).lie_h_e_nsmul, b.lie_h_e i i]; abel
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : IsAddTorsionFree L
i : ι
this : NoZeroSMulDivisors ℤ L
aux : (b.A i i - 2) • b.e i = 0
⊢ b.A i i = 2
have rwa : ∀ (aux : b.A i i - 2 = 0), b.A i i = 2
Tactic: rwa [IsAddTorsionFree.zsmul_eq_zero_iff_left (b.sl2 i).e_ne_zero, sub_eq_zero] at aux
Cleared hypotheses: aux
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : IsAddTorsionFree L
i : ι
this : NoZeroSMulDivisors ℤ L
aux : (b.A i i - 2) • b.e i = 0
rwa : ∀ (aux : b.A i i - 2 = 0), b.A i i = 2
⊢ b.A i i = 2
have rwa₁ : ∀ (aux : b.A i i = 2), b.A i i = 2
Tactic: rwa [IsAddTorsionFree.zsmul_eq_zero_iff_left (b.sl2 i).e_ne_zero, sub_eq_zero] at aux
Cleared hypotheses: aux
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
⊢ b.cartan.toSubmodule = Submodule.span R (range b.h)
have rw : Eq (α := Submodule R L) (toSubmodule (lieSpan R L (range b.h))) (Submodule.span R (range b.h))
Tactic: rw [b.cartan_eq_lieSpan]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
⊢ Eq (α := Submodule R L) (toSubmodule (lieSpan R L (range b.h))) (Submodule.span R (range b.h))
have hs : ∀ x ∈ range b.h, ∀ y ∈ range b.h, ⁅x, y⁆ = 0
Tactic: apply coe_lieSpan_eq_span_of_forall_lie_eq_zero
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
⊢ IsLieAbelian.{u_3} ↥b.cartan
have rw : ∀ x ∈ range b.h, ∀ y ∈ range b.h, ⁅x, y⁆ = 0
Tactic: rw [cartan_eq_lieSpan, isLieAbelian_lieSpan_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
⊢ b.cartan = lieSpan R L (range (-b.h))
have rw : b.cartan = lieSpan R L (range b.h)
Tactic: rw [← neg_range', lieSpan_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
⊢ Eq (α := LieSubalgebra R L) (lieSpan R L (range b.f ∪ range b.e)) ⊤
have rw : Eq (α := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) ⊤
Tactic: rw [union_comm, b.span_ef]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
rw : Eq (α := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) ⊤
⊢ Eq (α := LieSubalgebra R L) (lieSpan R L (range b.f ∪ range b.e)) ⊤
have rw₁ : Eq.{u_3 + 1} (α := LieSubalgebra R L) ⊤ ⊤
Tactic: rw [union_comm, b.span_ef]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
⊢ ⁅(-b.h) i, (-b.h) j⁆ = 0
have rw : ⁅-b.h i, (-b.h) j⁆ = 0
Tactic: rw [Pi.neg_apply, Pi.neg_apply, neg_lie, lie_neg, b.lie_h_h i j, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
rw : ⁅-b.h i, (-b.h) j⁆ = 0
⊢ ⁅(-b.h) i, (-b.h) j⁆ = 0
have rw₁ : ⁅-b.h i, -b.h j⁆ = 0
Tactic: rw [Pi.neg_apply, Pi.neg_apply, neg_lie, lie_neg, b.lie_h_h i j, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
rw : ⁅-b.h i, (-b.h) j⁆ = 0
rw₁ : ⁅-b.h i, -b.h j⁆ = 0
⊢ ⁅(-b.h) i, (-b.h) j⁆ = 0
have rw₂ : -⁅b.h i, -b.h j⁆ = 0
Tactic: rw [Pi.neg_apply, Pi.neg_apply, neg_lie, lie_neg, b.lie_h_h i j, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
rw : ⁅-b.h i, (-b.h) j⁆ = 0
rw₁ : ⁅-b.h i, -b.h j⁆ = 0
rw₂ : -⁅b.h i, -b.h j⁆ = 0
⊢ ⁅(-b.h) i, (-b.h) j⁆ = 0
have rw₃ : - -⁅b.h i, b.h j⁆ = 0
Tactic: rw [Pi.neg_apply, Pi.neg_apply, neg_lie, lie_neg, b.lie_h_h i j, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
rw : ⁅-b.h i, (-b.h) j⁆ = 0
rw₁ : ⁅-b.h i, -b.h j⁆ = 0
rw₂ : -⁅b.h i, -b.h j⁆ = 0
rw₃ : - -⁅b.h i, b.h j⁆ = 0
⊢ ⁅(-b.h) i, (-b.h) j⁆ = 0
have rw₄ : Eq.{u_3 + 1} (α := L) (- -0) 0
Tactic: rw [Pi.neg_apply, Pi.neg_apply, neg_lie, lie_neg, b.lie_h_h i j, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
rw : ⁅-b.h i, (-b.h) j⁆ = 0
rw₁ : ⁅-b.h i, -b.h j⁆ = 0
rw₂ : -⁅b.h i, -b.h j⁆ = 0
rw₃ : - -⁅b.h i, b.h j⁆ = 0
rw₄ : Eq.{u_3 + 1} (α := L) (- -0) 0
⊢ ⁅(-b.h) i, (-b.h) j⁆ = 0
have rw₅ : Eq.{u_3 + 1} (α := L) 0 0
Tactic: rw [Pi.neg_apply, Pi.neg_apply, neg_lie, lie_neg, b.lie_h_h i j, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
⊢ ⁅(-b.h) j, b.f i⁆ = b.A i j • b.f i
have rw : ⁅-b.h j, b.f i⁆ = b.A i j • b.f i
Tactic: rw [Pi.neg_apply, neg_lie, b.lie_h_f i j, neg_smul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
rw : ⁅-b.h j, b.f i⁆ = b.A i j • b.f i
⊢ ⁅(-b.h) j, b.f i⁆ = b.A i j • b.f i
have rw₁ : -⁅b.h j, b.f i⁆ = b.A i j • b.f i
Tactic: rw [Pi.neg_apply, neg_lie, b.lie_h_f i j, neg_smul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
rw : ⁅-b.h j, b.f i⁆ = b.A i j • b.f i
rw₁ : -⁅b.h j, b.f i⁆ = b.A i j • b.f i
⊢ ⁅(-b.h) j, b.f i⁆ = b.A i j • b.f i
have rw₂ : -(-b.A i j • b.f i) = b.A i j • b.f i
Tactic: rw [Pi.neg_apply, neg_lie, b.lie_h_f i j, neg_smul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
rw : ⁅-b.h j, b.f i⁆ = b.A i j • b.f i
rw₁ : -⁅b.h j, b.f i⁆ = b.A i j • b.f i
rw₂ : -(-b.A i j • b.f i) = b.A i j • b.f i
⊢ ⁅(-b.h) j, b.f i⁆ = b.A i j • b.f i
have rw₃ : - -(b.A i j • b.f i) = b.A i j • b.f i
Tactic: rw [Pi.neg_apply, neg_lie, b.lie_h_f i j, neg_smul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
rw : ⁅-b.h j, b.f i⁆ = b.A i j • b.f i
rw₁ : -⁅b.h j, b.f i⁆ = b.A i j • b.f i
rw₂ : -(-b.A i j • b.f i) = b.A i j • b.f i
rw₃ : - -(b.A i j • b.f i) = b.A i j • b.f i
⊢ ⁅(-b.h) j, b.f i⁆ = b.A i j • b.f i
have rw₄ : b.A i j • b.f i = b.A i j • b.f i
Tactic: rw [Pi.neg_apply, neg_lie, b.lie_h_f i j, neg_smul, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
⊢ ⁅(-b.h) j, b.e i⁆ = -b.A i j • b.e i
have rw : ⁅-b.h j, b.e i⁆ = -b.A i j • b.e i
Tactic: rw [Pi.neg_apply, neg_lie, b.lie_h_e, neg_smul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
rw : ⁅-b.h j, b.e i⁆ = -b.A i j • b.e i
⊢ ⁅(-b.h) j, b.e i⁆ = -b.A i j • b.e i
have rw₁ : -⁅b.h j, b.e i⁆ = -b.A i j • b.e i
Tactic: rw [Pi.neg_apply, neg_lie, b.lie_h_e, neg_smul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
rw : ⁅-b.h j, b.e i⁆ = -b.A i j • b.e i
rw₁ : -⁅b.h j, b.e i⁆ = -b.A i j • b.e i
⊢ ⁅(-b.h) j, b.e i⁆ = -b.A i j • b.e i
have rw₂ : -(b.A i j • b.e i) = -b.A i j • b.e i
Tactic: rw [Pi.neg_apply, neg_lie, b.lie_h_e, neg_smul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
rw : ⁅-b.h j, b.e i⁆ = -b.A i j • b.e i
rw₁ : -⁅b.h j, b.e i⁆ = -b.A i j • b.e i
rw₂ : -(b.A i j • b.e i) = -b.A i j • b.e i
⊢ ⁅(-b.h) j, b.e i⁆ = -b.A i j • b.e i
have rw₃ : -(b.A i j • b.e i) = -(b.A i j • b.e i)
Tactic: rw [Pi.neg_apply, neg_lie, b.lie_h_e, neg_smul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
h : i ≠ j
⊢ ⁅b.f i, b.e j⁆ = 0
have rw : -⁅b.e j, b.f i⁆ = 0
Tactic: rw [← lie_skew, neg_eq_zero, b.lie_e_f_ne j i h.symm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
h : i ≠ j
rw : -⁅b.e j, b.f i⁆ = 0
⊢ ⁅b.f i, b.e j⁆ = 0
have rw₁ : ⁅b.e j, b.f i⁆ = 0
Tactic: rw [← lie_skew, neg_eq_zero, b.lie_e_f_ne j i h.symm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
h : i ≠ j
rw : -⁅b.e j, b.f i⁆ = 0
rw₁ : ⁅b.e j, b.f i⁆ = 0
⊢ ⁅b.f i, b.e j⁆ = 0
have rw₂ : Eq.{u_3 + 1} (α := L) 0 0
Tactic: rw [← lie_skew, neg_eq_zero, b.lie_e_f_ne j i h.symm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : x ∈ b.cartan
u : L
hu : u ∈ range b.e
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, u⁆
have mem : ∀ (i : ι), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, b.e i⁆
Tactic: obtain ⟨i, rfl⟩ := hu
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : x ∈ b.cartan
i : ι
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, b.e i⁆
have mem : ∀ (hx : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x) (i : ι),
  Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, b.e i⁆
Tactic: rw [← mem_toSubmodule, coe_cartan_eq_span] at hx
Cleared hypotheses: hx, i
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
i : ι
v : L
hv : v ∈ range b.h
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v, b.e i⁆
have mem : ∀ (j : ι), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅b.h j, b.e i⁆
Tactic: obtain ⟨j, rfl⟩ := hv
Cleared hypotheses: v, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
i j : ι
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅b.h j, b.e i⁆
have mem : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) (b.A i j • b.e i)
Tactic: rw [b.lie_h_e]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
i : ι
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, b.e i⁆
have mem : ∀ (v : L) (hv : v ∈ range b.h), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v, b.e i⁆
Tactic: induction hx using Submodule.span_induction with
    | mem v hv =>
      obtain ⟨j, rfl⟩ := hv
      rw [b.lie_h_e]
      apply zsmul_mem <| subset_lieSpan <| mem_range_self i
    | zero => simp
    | add v w _ _ hv hw => simpa using add_mem hv hw
    | smul t v _ hv => simpa using LieSubalgebra.smul_mem _ t hv
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
i : ι
mem : ∀ (v : L) (hv : v ∈ range b.h), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v, b.e i⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, b.e i⁆
have mem₁ : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) (Bracket.bracket (L := L) 0 (b.e i))
Tactic: induction hx using Submodule.span_induction with
    | mem v hv =>
      obtain ⟨j, rfl⟩ := hv
      rw [b.lie_h_e]
      apply zsmul_mem <| subset_lieSpan <| mem_range_self i
    | zero => simp
    | add v w _ _ hv hw => simpa using add_mem hv hw
    | smul t v _ hv => simpa using LieSubalgebra.smul_mem _ t hv
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
i : ι
mem : ∀ (v : L) (hv : v ∈ range b.h), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v, b.e i⁆
mem₁ : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) (Bracket.bracket (L := L) 0 (b.e i))
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, b.e i⁆
have mem₂ : ∀ (v w : L),
  Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) v →
    Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) w →
      ∀ (hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v, b.e i⁆)
        (hw : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅w, b.e i⁆),
        Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v + w, b.e i⁆
Tactic: induction hx using Submodule.span_induction with
    | mem v hv =>
      obtain ⟨j, rfl⟩ := hv
      rw [b.lie_h_e]
      apply zsmul_mem <| subset_lieSpan <| mem_range_self i
    | zero => simp
    | add v w _ _ hv hw => simpa using add_mem hv hw
    | smul t v _ hv => simpa using LieSubalgebra.smul_mem _ t hv
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x
i : ι
mem : ∀ (v : L) (hv : v ∈ range b.h), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v, b.e i⁆
mem₁ : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) (Bracket.bracket (L := L) 0 (b.e i))
mem₂ :
  ∀ (v w : L),
    Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) v →
      Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) w →
        ∀ (hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v, b.e i⁆)
          (hw : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅w, b.e i⁆),
          Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v + w, b.e i⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, b.e i⁆
have mem₃ : ∀ (t : R) (v : L),
  Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) v →
    ∀ (hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v, b.e i⁆),
      Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅t • v, b.e i⁆
Tactic: induction hx using Submodule.span_induction with
    | mem v hv =>
      obtain ⟨j, rfl⟩ := hv
      rw [b.lie_h_e]
      apply zsmul_mem <| subset_lieSpan <| mem_range_self i
    | zero => simp
    | add v w _ _ hv hw => simpa using add_mem hv hw
    | smul t v _ hv => simpa using LieSubalgebra.smul_mem _ t hv
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : x ∈ b.cartan
u v : L
hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) u
hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) v
hu' : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, u⁆
hv' : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, v⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, ⁅u, v⁆⁆
have lie : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) (⁅u, ⁅x, v⁆⁆ - ⁅v, ⁅x, u⁆⁆)
Tactic: rw [leibniz_lie, ← lie_skew _ v, neg_add_eq_sub]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : x ∈ b.cartan
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) y
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, y⁆
have mem : ∀ (u : L) (hu : u ∈ range b.e), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, u⁆
Tactic: induction hy using lieSpan_induction with
  | mem u hu =>
    obtain ⟨i, rfl⟩ := hu
    rw [← mem_toSubmodule, coe_cartan_eq_span] at hx
    induction hx using Submodule.span_induction with
    | mem v hv =>
      obtain ⟨j, rfl⟩ := hv
      rw [b.lie_h_e]
      apply zsmul_mem <| subset_lieSpan <| mem_range_self i
    | zero => simp
    | add v w _ _ hv hw => simpa using add_mem hv hw
    | smul t v _ hv => simpa using LieSubalgebra.smul_mem _ t hv
  | zero => simp
  | add u v _ _ hu hv => simpa using add_mem hu hv
  | smul t u _ hu => simpa using LieSubalgebra.smul_mem _ t hu
  | lie u v hu hv hu' hv' =>
    rw [leibniz_lie, ← lie_skew _ v, neg_add_eq_sub]
    exact sub_mem (LieSubalgebra.lie_mem _ hu hv') (LieSubalgebra.lie_mem _ hv hu')
Cleared hypotheses: hy