awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 ⋯)
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) 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) y hy) =
    0
have refine_2₁ : 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) 0 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
-- 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
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 ⋯)
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u ⋯))
      0
refine_2₁ :
  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
⊢ 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 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 sorry)
        (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 sorry)
        (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 sorry)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) (u + v) 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
-- 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
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
⊢ ⁅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
have refine_2 : ∀ (hu : ⁅u, y⁆ = 0) (hv : ⁅v, y⁆ = 0), ⁅u, y⁆ + ⁅v, y⁆ = 0
Tactic: simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, add_lie] 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 : L
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
t : R
u : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
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
⊢ ⁅Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) (t • u) ⋯,
      Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y hy⁆ =
    0
have hu₁ : ⁅u, y⁆ = 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 : 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
⊢ ⁅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
have refine_2 : ∀ (hu : ⁅u, y⁆ = 0) (hv : ⁅v, y⁆ = 0), ⁅⁅u, v⁆, y⁆ = 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 : 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
have refine_2 : ∀ (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 sorry)
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y hy) =
    0
Tactic: induction hx using lieSpan_induction with
    | mem w hw =>
      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]
    | zero => simp [Subtype.ext_iff]
    | add u v _ _ hu hv =>
      simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, add_lie] 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 ⊢
      simp [hu, hv]
Cleared hypotheses: hx
-- 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 : 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
refine_2 :
  ∀ (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
⊢ ⁅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
have refine_2₁ : Bracket.bracket (L := ↥(lieSpan R L s))
    (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) 0 sorry)
    (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y hy) =
  0
Tactic: induction hx using lieSpan_induction with
    | mem w hw =>
      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]
    | zero => simp [Subtype.ext_iff]
    | add u v _ _ hu hv =>
      simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, add_lie] 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 ⊢
      simp [hu, hv]
Cleared hypotheses: hx
-- 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 : 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
refine_2 :
  ∀ (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
refine_2₁ :
  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
⊢ ⁅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
have refine_2₂ : ∀ (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),
  ⁅Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) (u + v) sorry,
      Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) y hy⁆ =
    0
Tactic: induction hx using lieSpan_induction with
    | mem w hw =>
      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]
    | zero => simp [Subtype.ext_iff]
    | add u v _ _ hu hv =>
      simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, add_lie] 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 ⊢
      simp [hu, hv]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian.{v} ↥I ↔ I ≤ LieModule.ker R L ↥I
have refine_1 : ∀ (hI : IsLieAbelian.{v} ↥I) (x : L) (hx : x ∈ I),
  Eq (α := Module.End R ↥I) ((toEnd R L ↥I : (a : L) → Module.End R ↥I) x : Module.End R ↥I) (0 : Module.End R ↥I)
Tactic: refine ⟨fun hI x hx ↦ LieHom.mem_ker.mpr ?_, fun h ↦ ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
refine_1 :
  ∀ (hI : IsLieAbelian.{v} ↥I) (x : L) (hx : x ∈ I),
    Eq (α := Module.End R ↥I) ((toEnd R L ↥I : (a : L) → Module.End R ↥I) x : Module.End R ↥I) (0 : Module.End R ↥I)
⊢ IsLieAbelian.{v} ↥I ↔ I ≤ LieModule.ker R L ↥I
have refine_2 : ∀ (h : I ≤ LieModule.ker R L ↥I) (x x : ↥I) (x : L) (hx : x ∈ I) (y : L) (hy : y ∈ I),
  ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx, Subtype.mk (p := fun (x : L) ↦ x ∈ I) y hy⁆ = 0
Tactic: refine ⟨fun hI x hx ↦ LieHom.mem_ker.mpr ?_, fun h ↦ ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
hI : IsLieAbelian.{v} ↥I
x : L
hx : x ∈ I
⊢ Eq (α := Module.End R ↥I) ((toEnd R L ↥I : (a : L) → Module.End R ↥I) x : Module.End R ↥I) (0 : Module.End R ↥I)
have refine_1 : ∀ (y : ↥I),
  Eq.{v + 1} (α := L) (↑((((toEnd R L ↥I : (a : L) → Module.End R ↥I) x : Module.End R ↥I) : (a : ↥I) → ↥I) y) : L)
    (↑((0 : (a : ↥I) → ↥I) y) : L)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
hI : IsLieAbelian.{v} ↥I
x : L
hx : x ∈ I
y : ↥I
⊢ Eq.{v + 1} (α := L) (↑((((toEnd R L ↥I : (a : L) → Module.End R ↥I) x : Module.End R ↥I) : (a : ↥I) → ↥I) y) : L)
    (↑((0 : (a : ↥I) → ↥I) y) : L)
have this : ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx, y⁆ = 0
Tactic: have := IsTrivial.trivial (⟨x, hx⟩ : I) y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
hI : IsLieAbelian.{v} ↥I
x : L
hx : x ∈ I
y : ↥I
this : ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx, y⁆ = 0
⊢ Eq.{v + 1} (α := L) (↑((((toEnd R L ↥I : (a : L) → Module.End R ↥I) x : Module.End R ↥I) : (a : ↥I) → ↥I) y) : L)
    (↑((0 : (a : ↥I) → ↥I) y) : L)
have this₁ : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), y⁆ = 0
Tactic: rw [LieIdeal.coe_bracket_of_module] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
⊢ IsFaithful R L M ↔ Eq (α := LieIdeal R L) (LieModule.ker R L M) ⊥
have rw : (∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0) ↔
  ∀ (m : L),
    Membership.mem (γ := LieSubmodule R L L) (LieModule.ker R L M) m ↔ Membership.mem (γ := LieSubmodule R L L) ⊥ m
Tactic: rw [isFaithful_iff', LieSubmodule.ext_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
x y : M
hx : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} x
hy : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} y
z : L
⊢ ⁅z, x + y⁆ = 0
have rw : ⁅z, x⁆ + ⁅z, y⁆ = 0
Tactic: rw [lie_add, hx, hy, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
x y : M
hx : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} x
hy : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} y
z : L
rw : ⁅z, x⁆ + ⁅z, y⁆ = 0
⊢ ⁅z, x + y⁆ = 0
have rw₁ : 0 + ⁅z, y⁆ = 0
Tactic: rw [lie_add, hx, hy, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
x y : M
hx : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} x
hy : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} y
z : L
rw : ⁅z, x⁆ + ⁅z, y⁆ = 0
rw₁ : 0 + ⁅z, y⁆ = 0
⊢ ⁅z, x + y⁆ = 0
have rw₂ : HAdd.hAdd (α := M) 0 0 = 0
Tactic: rw [lie_add, hx, hy, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
x y : M
hx : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} x
hy : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} y
z : L
rw : ⁅z, x⁆ + ⁅z, y⁆ = 0
rw₁ : 0 + ⁅z, y⁆ = 0
rw₂ : HAdd.hAdd (α := M) 0 0 = 0
⊢ ⁅z, x + y⁆ = 0
have rw₃ : Eq.{w + 1} (α := M) 0 0
Tactic: rw [lie_add, hx, hy, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
c : R
x : M
hx : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} x
y : L
⊢ ⁅y, c • x⁆ = 0
have rw : c • ⁅y, x⁆ = 0
Tactic: rw [lie_smul, hx, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
c : R
x : M
hx : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} x
y : L
rw : c • ⁅y, x⁆ = 0
⊢ ⁅y, c • x⁆ = 0
have rw₁ : HSMul.hSMul (β := M) c 0 = 0
Tactic: rw [lie_smul, hx, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
c : R
x : M
hx : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} x
y : L
rw : c • ⁅y, x⁆ = 0
rw₁ : HSMul.hSMul (β := M) c 0 = 0
⊢ ⁅y, c • x⁆ = 0
have rw₂ : Eq.{w + 1} (α := M) 0 0
Tactic: rw [lie_smul, hx, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
x : L
m : M
hm : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} m
y : L
⊢ ⁅y, ⁅x, m⁆⁆ = 0
have rw : Eq.{w + 1} (α := M) ⁅y, 0⁆ 0
Tactic: rw [hm, lie_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Abelian (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
x : L
m : M
hm : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ = 0} m
y : L
rw : Eq.{w + 1} (α := M) ⁅y, 0⁆ 0
⊢ ⁅y, ⁅x, m⁆⁆ = 0
have rw₁ : Eq.{w + 1} (α := M) 0 0
Tactic: rw [hm, lie_zero]