awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b c : A
⊢ HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (b * b)) :
              AddMonoid.End A)
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * a)) :
              AddMonoid.End A) +
          HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
            (-Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (a * a)) :
              AddMonoid.End A)
            (-Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (b * b)) :
              AddMonoid.End A) +
        (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (c * c)) :
              AddMonoid.End A)
            (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * a)) :
              AddMonoid.End A) +
          HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
            (-Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (a * a)) :
              AddMonoid.End A)
            (-Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
                  ((L : (a : A) → AddMonoid.End A) (c * c)) :
              AddMonoid.End A)) +
      (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (c * c)) :
            AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * b)) :
            AddMonoid.End A) +
        HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
          (-Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (b * b)) :
            AddMonoid.End A)
          (-Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (c * c)) :
            AddMonoid.End A)) =
    0

Tactic:
abel
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b c : A
symm :
  0 =
    HSMul.hSMul (α := ℕ) 2
      (HAdd.hAdd (β := AddMonoid.End A)
        (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * c)) :
            AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (c * a)) :
            AddMonoid.End A))
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (a * b)) :
          AddMonoid.End A))
⊢ HSMul.hSMul (α := ℕ) 2
      (HAdd.hAdd (β := AddMonoid.End A)
        (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * c)) :
            AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (c * a)) :
            AddMonoid.End A))
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (a * b)) :
          AddMonoid.End A)) =
    0

Tactic:
symm
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b c : A
rw rw₁ : Eq.{u_1 + 1} (α := AddMonoid.End A) 0 0
⊢ Eq (α := AddMonoid.End A) (0 : AddMonoid.End A)
    (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (a + b + c) : AddMonoid.End A)
        ((L : (a : A) → AddMonoid.End A) ((a + b + c) * (a + b + c))) :
      AddMonoid.End A)

Tactic:
rw [(commute_lmul_lmul_sq (a + b + c)).lie_eq]

Premises used: Commute.lie_eq, commute_lmul_lmul_sq, HAdd.hAdd
-- Module: Mathlib.Algebra.Jordan.Basic
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b c : A
b₁ :
  Eq (α := AddMonoid.End A) (0 : AddMonoid.End A)
    (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (a + b + c) : AddMonoid.End A)
        ((L : (a : A) → AddMonoid.End A) ((a + b + c) * (a + b + c))) :
      AddMonoid.End A)
b₂ :
  Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) (a + b + c) : AddMonoid.End A)
      ((L : (a : A) → AddMonoid.End A) ((a + b + c) * (a + b + c))) =
    HSMul.hSMul (α := ℕ) 2
      (HAdd.hAdd (β := AddMonoid.End A)
        (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * c)) :
            AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (c * a)) :
            AddMonoid.End A))
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (a * b)) :
          AddMonoid.End A))
⊢ 0 =
    HSMul.hSMul (α := ℕ) 2
      (HAdd.hAdd (β := AddMonoid.End A)
        (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * c)) :
            AddMonoid.End A)
          (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (c * a)) :
            AddMonoid.End A))
        (Bracket.bracket («L» := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A)
            ((L : (a : A) → AddMonoid.End A) (a * b)) :
          AddMonoid.End A))

Tactic:
calc
    0 = ⁅L (a + b + c), L ((a + b + c) * (a + b + c))⁆ := by
      rw [(commute_lmul_lmul_sq (a + b + c)).lie_eq]
    _ = _ := by rw [aux0, aux1, aux2, aux3, nsmul_add, nsmul_add]

Premises used: AddMonoid.End.mulLeft, HMul.hMul, HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
L : Type v
M : Type w
inst : Bracket L M
inst_1 : Zero M
inst_2 : LieModule.IsTrivial L M
x : L
m : M
⊢ ⁅x, m⁆ = 0

Tactic:
LieModule.IsTrivial.trivial x m

Premises used: LieModule.IsTrivial.trivial
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
L : Type u_1
M : Type u_2
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : Subsingleton L
x : L
m : M
rw : Bracket.bracket.{u_1, u_2} (L := L) 0 m = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) 0 0
⊢ ⁅x, m⁆ = 0

Tactic:
rw [Subsingleton.eq_zero x, zero_lie]

Premises used: zero_lie, Subsingleton.eq_zero
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
L : Type u_1
M : Type u_2
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : Subsingleton M
x : L
m : M
simp_rw : Eq.{u_2 + 1} (α := M) ⁅x, 0⁆ 0
⊢ ⁅x, m⁆ = 0

Tactic:
simp_rw [Subsingleton.eq_zero m, lie_zero]

Premises used: lie_zero, Subsingleton.eq_zero
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h : LieModule.IsTrivial L ↥I
x y : ↥I
⊢ ⁅x, y⁆ = 0

Tactic:
apply h.trivial

Premises used: LieModule.IsTrivial.trivial
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : Injective.{v + 1, w + 1} (α := L₁) (β := L₂) (⇑f : (a : L₁) → L₂)
h : IsLieAbelian L₂
⊢ IsLieAbelian L₁

Tactic:
{ trivial := fun x y => h₁ <|
      calc
        f ⁅x, y⁆ = ⁅f x, f y⁆ := LieHom.map_lie f x y
        _ = 0 := trivial_lie_zero _ _ _ _
        _ = f 0 := (map_zero _).symm }

Premises used: Trans.trans, LieHom.map_lie, map_zero, LieModule.IsTrivial.mk, trivial_lie_zero, Eq.symm, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : Surjective.{v + 1, w + 1} (α := L₁) (β := L₂) (⇑f : (a : L₁) → L₂)
h₂ : IsLieAbelian L₁
x y : L₂
obtain : ∀ (u : L₁), Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) u : L₂) y = 0
⊢ ⁅x, y⁆ = 0

Tactic:
obtain ⟨u, rfl⟩ := h₁ x

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : Surjective.{v + 1, w + 1} (α := L₁) (β := L₂) (⇑f : (a : L₁) → L₂)
h₂ : IsLieAbelian L₁
y : L₂
u : L₁
obtain :
  ∀ (v : L₁),
    Eq.{w + 1} (α := L₂) (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) u : L₂) ((f : (a : L₁) → L₂) v) : L₂) (0 : L₂)
⊢ Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) u : L₂) y = 0

Tactic:
obtain ⟨v, rfl⟩ := h₁ y

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : Surjective.{v + 1, w + 1} (α := L₁) (β := L₂) (⇑f : (a : L₁) → L₂)
h₂ : IsLieAbelian L₁
u v : L₁
rw : Eq.{w + 1} (α := L₂) ((f : (a : L₁) → L₂) ⁅u, v⁆ : L₂) (0 : L₂)
rw₁ : Eq.{w + 1} (α := L₂) ((f : (a : L₁) → L₂) 0 : L₂) (0 : L₂)
rw₂ rw₃ : Eq.{w + 1} (α := L₂) 0 0
⊢ Eq.{w + 1} (α := L₂) (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) u : L₂) ((f : (a : L₁) → L₂) v) : L₂) (0 : L₂)

Tactic:
rw [← LieHom.map_lie, trivial_lie_zero, map_zero]

Premises used: LieHom.map_lie, map_zero, trivial_lie_zero
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
⊢ IsLieAbelian L₁ ↔ IsLieAbelian L₂

Tactic:
⟨e.symm.injective.isLieAbelian, e.injective.isLieAbelian⟩

Premises used: LieEquiv.injective, Function.Injective.isLieAbelian, Iff.intro, LieEquiv.symm
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
A : Type v
inst : Ring A
⊢ IsLieAbelian A ↔ ∀ (a b : A), ⁅a, b⁆ = 0

Tactic:
have : IsLieAbelian A ↔ ∀ a b : A, ⁅a, b⁆ = 0 := ⟨(·.trivial), (⟨·⟩)⟩
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
A : Type v
inst : Ring A
this : IsLieAbelian A ↔ ∀ (a b : A), ⁅a, b⁆ = 0
⊢ IsMulCommutative A ↔ IsLieAbelian A

Tactic:
simp [this, isMulCommutative_iff, LieRing.of_associative_ring_bracket, sub_eq_zero]

Premises used: sub_eq_zero, LieRing.of_associative_ring_bracket, isMulCommutative_iff
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
⊢ IsLieAbelian.{u_2} ↥(lieSpan R L s) ↔ ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0

Tactic:
⟨fun h x hx y hy ↦ ?_, fun h ↦ ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ?_⟩⟩

Premises used: Bracket.bracket, Subtype.mk, LieModule.IsTrivial.mk, Iff.intro, _private.0.LieSubalgebra.isLieAbelian_lieSpan_iff.match_1, OfNat.ofNat, Eq
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
refine_1 : ∀ (h : IsLieAbelian.{u_2} ↥(lieSpan R L s)) (x : L) (hx : x ∈ s) (y : L) (hy : y ∈ s), ⁅x, y⁆ = 0
refine_2 :
  ∀ (h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0) (x x : ↥(lieSpan R L s)) (x : L)
    (hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) (y : L)
    (hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y),
    ⁅Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) x hx,
        Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y hy⁆ =
      0
⊢ IsLieAbelian.{u_2} ↥(lieSpan R L s) ↔ ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0

Tactic:
refine ⟨fun h x hx y hy ↦ ?_, fun h ↦ ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ?_⟩⟩
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : IsLieAbelian.{u_2} ↥(lieSpan R L s)
x : L
hx : x ∈ s
y : L
hy : y ∈ s
x' : ↥(lieSpan R L s) := Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) x ⋯
y' : ↥(lieSpan R L s) := Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y ⋯
this : ⁅x', y'⁆ = 0
⊢ ⁅x, y⁆ = 0

Tactic:
simpa [x', y', Subtype.ext_iff] using this

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : IsLieAbelian.{u_2} ↥(lieSpan R L s)
x : L
hx : x ∈ s
y : L
hy : y ∈ s
x' : ↥(lieSpan R L s) := Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) x ⋯
y' : ↥(lieSpan R L s) := Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y ⋯
refine_1 : ⁅x', y'⁆ = 0
⊢ ⁅x, y⁆ = 0

Tactic:
suffices ⁅x', y'⁆ = 0 by simpa [x', y', Subtype.ext_iff] using this
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : IsLieAbelian.{u_2} ↥(lieSpan R L s)
x : L
hx : x ∈ s
y : L
hy : y ∈ s
x' : ↥(lieSpan R L s) := Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) x ⋯
y' : ↥(lieSpan R L s) := Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y ⋯
⊢ ⁅x', y'⁆ = 0

Tactic:
simp [trivial_lie_zero]

Premises used: trivial_lie_zero
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
u : L
hu : u ∈ s
⊢ Eq (α := ↥(lieSpan R L s))
    (Bracket.bracket (L := ↥(lieSpan R L s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) w ⋯)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u ⋯))
    0

Tactic:
simpa [Subtype.ext_iff] using h w hw u hu

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
⊢ Eq (α := ↥(lieSpan R L s))
    (Bracket.bracket (L := ↥(lieSpan R L s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) w ⋯)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) 0 ⋯))
    0

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) v
hu :
  Bracket.bracket (L := ↥(lieSpan R L s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) w ⋯)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u hx) =
    0
hv :
  Bracket.bracket (L := ↥(lieSpan R L s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) w ⋯)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) v hy) =
    0
refine_2 : ∀ (hu : ⁅w, u⁆ = 0) (hv : ⁅w, v⁆ = 0), ⁅w, u⁆ + ⁅w, v⁆ = 0
⊢ Bracket.bracket (L := ↥(lieSpan R L s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) w ⋯)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) (u + v) ⋯) =
    0

Tactic:
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, lie_add] at hu hv ⊢

Premises used: Subtype.ext_iff, LieSubalgebra.coe_bracket, ZeroMemClass.coe_zero, lie_add
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) v
hu : ⁅w, u⁆ = 0
hv : ⁅w, v⁆ = 0
⊢ ⁅w, u⁆ + ⁅w, v⁆ = 0

Tactic:
simp [hu, hv]
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
t : R
u : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
hu :
  Bracket.bracket (L := ↥(lieSpan R L s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) w ⋯)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u hx) =
    0
⊢ ⁅w, u⁆ = 0

Tactic:
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu

Premises used: Subtype.ext_iff, LieSubalgebra.coe_bracket, ZeroMemClass.coe_zero
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
t : R
u : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
hu : ⁅w, u⁆ = 0
⊢ Bracket.bracket (L := ↥(lieSpan R L s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) w ⋯)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) (t • u) ⋯) =
    0

Tactic:
simp [Subtype.ext_iff, hu]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) v
hu :
  Bracket.bracket (L := ↥(lieSpan R L s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) w ⋯)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u hx) =
    0
hv :
  Bracket.bracket (L := ↥(lieSpan R L s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) w ⋯)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) v hy) =
    0
refine_2 : ∀ (hu : ⁅w, u⁆ = 0) (hv : ⁅w, v⁆ = 0), ⁅w, ⁅u, v⁆⁆ = 0
⊢ Bracket.bracket (L := ↥(lieSpan R L s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) w ⋯)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁅u, v⁆ ⋯) =
    0

Tactic:
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu hv ⊢

Premises used: Subtype.ext_iff, LieSubalgebra.coe_bracket, ZeroMemClass.coe_zero
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) v
hu : ⁅w, u⁆ = 0
hv : ⁅w, v⁆ = 0
refine_2 : ⁅⁅w, u⁆, v⁆ + ⁅u, ⁅w, v⁆⁆ = 0
⊢ ⁅w, ⁅u, v⁆⁆ = 0

Tactic:
rw [leibniz_lie]

Premises used: leibniz_lie
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) v
hu : ⁅w, u⁆ = 0
hv : ⁅w, v⁆ = 0
⊢ ⁅⁅w, u⁆, v⁆ + ⁅u, ⁅w, v⁆⁆ = 0

Tactic:
simp [hu, hv]
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y : L
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
⊢ Bracket.bracket (L := ↥(lieSpan R L s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) 0 ⋯)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y hy) =
    0

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y : L
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
hy_1 : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) v
hu :
  ⁅Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u hx,
      Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y hy⁆ =
    0
hv :
  ⁅Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) v hy_1,
      Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y hy⁆ =
    0
refine_2 : ∀ (hu : ⁅u, y⁆ = 0) (hv : ⁅v, y⁆ = 0), ⁅u, y⁆ + ⁅v, y⁆ = 0
⊢ ⁅Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) (u + v) ⋯,
      Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y hy⁆ =
    0

Tactic:
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, add_lie] at hu hv ⊢

Premises used: Subtype.ext_iff, LieSubalgebra.coe_bracket, ZeroMemClass.coe_zero, add_lie
-- Module: Mathlib.Algebra.Lie.Abelian
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 x_2 : ↥(lieSpan R L s)
x y : L
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
hy_1 : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) v
hu : ⁅u, y⁆ = 0
hv : ⁅v, y⁆ = 0
⊢ ⁅u, y⁆ + ⁅v, y⁆ = 0

Tactic:
simp [hu, hv]