awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅HAdd.hAdd (β := AddMonoid.End A)
        (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A))
        ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A),
      (L : (a : A) → AddMonoid.End A) (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * c))⁆ =
    ⁅HAdd.hAdd (β := AddMonoid.End A)
        (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
          ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A))
        ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A),
      HAdd.hAdd (β := AddMonoid.End A)
              (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
                ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A))
              ((L : (a : A) → AddMonoid.End A) (c * c) : AddMonoid.End A) +
            HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A) +
          HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (c * a) : AddMonoid.End A) +
        HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A)⁆
have rw : ⁅HAdd.hAdd (β := AddMonoid.End A)
      (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
        ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A))
      ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A),
    HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
      ((L : (a : A) → AddMonoid.End A) (a * a + a * b + a * c + (b * a + b * b + b * c)) : AddMonoid.End A)
      ((L : (a : A) → AddMonoid.End A) (c * a + c * b + c * c) : AddMonoid.End A)⁆ =
  ⁅HAdd.hAdd (β := AddMonoid.End A)
      (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
        ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A))
      ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A),
    HAdd.hAdd (β := AddMonoid.End A)
            (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A))
            ((L : (a : A) → AddMonoid.End A) (c * c) : AddMonoid.End A) +
          HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A) +
        HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (c * a) : AddMonoid.End A) +
      HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (b * c) : AddMonoid.End A)⁆
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b c : 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
have 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))
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b c : A
⊢ 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)
have rw : Eq.{u_1 + 1} (α := AddMonoid.End A) 0 0
Tactic: rw [(commute_lmul_lmul_sq (a + b + c)).lie_eq]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b c : 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))) =
    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))
have rw : ⁅HAdd.hAdd (β := AddMonoid.End A)
      (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A) ((L : (a : A) → AddMonoid.End A) a : AddMonoid.End A)
        ((L : (a : A) → AddMonoid.End A) b : AddMonoid.End A))
      ((L : (a : A) → AddMonoid.End A) c : AddMonoid.End A),
    HAdd.hAdd (β := AddMonoid.End A)
            (HAdd.hAdd (α := AddMonoid.End A) (β := AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (a * a) : AddMonoid.End A)
              ((L : (a : A) → AddMonoid.End A) (b * b) : AddMonoid.End A))
            ((L : (a : A) → AddMonoid.End A) (c * c) : AddMonoid.End A) +
          HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (a * b) : AddMonoid.End A) +
        HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (c * a) : AddMonoid.End A) +
      HSMul.hSMul (α := ℕ) (β := AddMonoid.End A) 2 ((L : (a : A) → AddMonoid.End A) (b * c) : 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))
Tactic: rw [aux0, aux1, aux2, aux3, nsmul_add, nsmul_add]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalNonAssocCommRing A
inst_1 : IsCommJordan A
a b c : 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))
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Jordan.Basic (goal)
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)
⊢ 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))
have 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))
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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
⊢ ⁅x, m⁆ = 0
have rw : Bracket.bracket.{u_1, u_2} (L := L) 0 m = 0
Tactic: rw [Subsingleton.eq_zero x, zero_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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
⊢ ⁅x, m⁆ = 0
have rw₁ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [Subsingleton.eq_zero x, zero_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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
⊢ ⁅x, m⁆ = 0
have simp_rw : Eq.{u_2 + 1} (α := M) ⁅x, 0⁆ 0
Tactic: simp_rw [Subsingleton.eq_zero m, lie_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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₂
⊢ ⁅x, y⁆ = 0
have obtain : ∀ (u : L₁), Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) u : L₂) y = 0
Tactic: obtain ⟨u, rfl⟩ := h₁ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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₁
⊢ Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) u : L₂) y = 0
have 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₂)
Tactic: obtain ⟨v, rfl⟩ := h₁ y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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₁
⊢ Eq.{w + 1} (α := L₂) (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) u : L₂) ((f : (a : L₁) → L₂) v) : L₂) (0 : L₂)
have rw : Eq.{w + 1} (α := L₂) ((f : (a : L₁) → L₂) ⁅u, v⁆ : L₂) (0 : L₂)
Tactic: rw [← LieHom.map_lie, trivial_lie_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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₂)
⊢ Eq.{w + 1} (α := L₂) (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) u : L₂) ((f : (a : L₁) → L₂) v) : L₂) (0 : L₂)
have rw₁ : Eq.{w + 1} (α := L₂) ((f : (a : L₁) → L₂) 0 : L₂) (0 : L₂)
Tactic: rw [← LieHom.map_lie, trivial_lie_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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₂)
⊢ Eq.{w + 1} (α := L₂) (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) u : L₂) ((f : (a : L₁) → L₂) v) : L₂) (0 : L₂)
have rw₂ : Eq.{w + 1} (α := L₂) 0 0
Tactic: rw [← LieHom.map_lie, trivial_lie_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (hypothesis)
Goal:
A : Type v
inst : Ring A
⊢ IsMulCommutative A ↔ IsLieAbelian A
have this : IsLieAbelian A ↔ ∀ (a b : A), ⁅a, b⁆ = 0
Tactic: have : IsLieAbelian A ↔ ∀ a b : A, ⁅a, b⁆ = 0 := ⟨(·.trivial), (⟨·⟩)⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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
have refine_1 : ∀ (h : IsLieAbelian.{u_2} ↥(lieSpan R L s)) (x : L) (hx : x ∈ s) (y : L) (hy : y ∈ s), ⁅x, y⁆ = 0
Tactic: refine ⟨fun h x hx y hy ↦ ?_, fun h ↦ ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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
⊢ IsLieAbelian.{u_2} ↥(lieSpan R L s) ↔ ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
have 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
Tactic: refine ⟨fun h x hx y hy ↦ ?_, fun h ↦ ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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
have refine_1 : ⁅x', y'⁆ = 0
Tactic: suffices ⁅x', y'⁆ = 0 by simpa [x', y', Subtype.ext_iff] using this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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
⊢ 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
have refine_2 : ∀ (hu : ⁅w, u⁆ = 0) (hv : ⁅w, v⁆ = 0), ⁅w, u⁆ + ⁅w, v⁆ = 0
Tactic: simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, lie_add] at hu hv ⊢
Cleared hypotheses: hu, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (hypothesis)
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
⊢ 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
have hu₁ : ⁅w, u⁆ = 0
Tactic: simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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
⊢ 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
have refine_2 : ∀ (hu : ⁅w, u⁆ = 0) (hv : ⁅w, v⁆ = 0), ⁅w, ⁅u, v⁆⁆ = 0
Tactic: simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu hv ⊢
Cleared hypotheses: hu, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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⁆⁆ = 0
have refine_2 : ⁅⁅w, u⁆, v⁆ + ⁅u, ⁅w, v⁆⁆ = 0
Tactic: rw [leibniz_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
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
w : L
hw : w ∈ 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) y hy) =
    0
have refine_2 : ∀ (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 sorry)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u sorry))
    0
Tactic: induction hy using lieSpan_induction with
      | mem u hu => simpa [Subtype.ext_iff] using h w hw u hu
      | zero => simp [Subtype.ext_iff]
      | add u v _ _ hu hv =>
        simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, lie_add] at hu hv ⊢
        simp [hu, hv]
      | smul t u _ hu =>
        simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu
        simp [Subtype.ext_iff, hu]
      | lie u v _ _ hu hv =>
        simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu hv ⊢
        rw [leibniz_lie]
        simp [hu, hv]
Cleared hypotheses: hy