awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
this :
  ∀ {x y : L},
    Membership.mem (γ := Submodule R L) (span R s) x →
      Membership.mem (γ := Submodule R L) (span R s) y → Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
⊢ Eq (α := Submodule R L) (toSubmodule (lieSpan R L s)) (span R s)
have refine : LE.le (α := Submodule R L) (toSubmodule (lieSpan R L s)) (span R s)
Tactic: refine le_antisymm ?_ submodule_span_le_lieSpan
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
this :
  ∀ {x y : L},
    Membership.mem (γ := Submodule R L) (span R s) x →
      Membership.mem (γ := Submodule R L) (span R s) y → Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
⊢ LE.le (α := LieSubalgebra R L) (lieSpan R L s)
    (let __src : Submodule R L := span R s;
    { toSubmodule := __src, lie_mem' := ⋯ })
have rw : s ⊆
  (↑(let __src : Submodule R L := span R s;
      { toSubmodule := __src, lie_mem' := sorry }) :
    Set L)
Tactic: rw [lieSpan_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
⊢ Eq (α := Submodule R L) (toSubmodule (lieSpan R L s)) (span R s)
have suffices : ∀ {x y : L},
  Membership.mem (γ := Submodule R L) (span R s) x →
    Membership.mem (γ := Submodule R L) (span R s) y → Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
Tactic: suffices ∀ {x y}, x ∈ span R s → y ∈ span R s → ⁅x, y⁆ ∈ span R s by
    refine le_antisymm ?_ submodule_span_le_lieSpan
    change _ ≤ ({ span R s with lie_mem' := this } : LieSubalgebra R L)
    rw [lieSpan_le]
    exact subset_span
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x y : L
hx : Membership.mem (γ := Submodule R L) (span R s) x
hy : Membership.mem (γ := Submodule R L) (span R s) y
⊢ Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
have mem_mem : ∀ (x y : L) (hx : x ∈ s) (hy : y ∈ s), Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
Tactic: induction hx, hy using span_induction₂ with
  | mem_mem x y hx hy => simp [hs x hx y hy]
  | zero_left y hy => simp
  | zero_right x hx => simp
  | add_left x y z _ _ _ hx hy => simp [add_mem hx hy]
  | add_right x y z _ _ _ hx hy => simp [add_mem hx hy]
  | smul_left r x y _ _ h => simp [smul_mem _ r h]
  | smul_right r x y _ _ h => simp [smul_mem _ r h]
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x y : L
hx : Membership.mem (γ := Submodule R L) (span R s) x
hy : Membership.mem (γ := Submodule R L) (span R s) y
mem_mem : ∀ (x y : L) (hx : x ∈ s) (hy : y ∈ s), Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
⊢ Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
have zero_left : ∀ (y : L) (hy : Membership.mem (γ := Submodule R L) (span R s) y),
  Membership.mem (γ := Submodule R L) (span R s) (Bracket.bracket (L := L) 0 y)
Tactic: induction hx, hy using span_induction₂ with
  | mem_mem x y hx hy => simp [hs x hx y hy]
  | zero_left y hy => simp
  | zero_right x hx => simp
  | add_left x y z _ _ _ hx hy => simp [add_mem hx hy]
  | add_right x y z _ _ _ hx hy => simp [add_mem hx hy]
  | smul_left r x y _ _ h => simp [smul_mem _ r h]
  | smul_right r x y _ _ h => simp [smul_mem _ r h]
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x y : L
hx : Membership.mem (γ := Submodule R L) (span R s) x
hy : Membership.mem (γ := Submodule R L) (span R s) y
mem_mem : ∀ (x y : L) (hx : x ∈ s) (hy : y ∈ s), Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
zero_left :
  ∀ (y : L) (hy : Membership.mem (γ := Submodule R L) (span R s) y),
    Membership.mem (γ := Submodule R L) (span R s) (Bracket.bracket (L := L) 0 y)
⊢ Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
have zero_right : ∀ (x : L) (hx : Membership.mem (γ := Submodule R L) (span R s) x), Membership.mem (γ := Submodule R L) (span R s) ⁅x, 0⁆
Tactic: induction hx, hy using span_induction₂ with
  | mem_mem x y hx hy => simp [hs x hx y hy]
  | zero_left y hy => simp
  | zero_right x hx => simp
  | add_left x y z _ _ _ hx hy => simp [add_mem hx hy]
  | add_right x y z _ _ _ hx hy => simp [add_mem hx hy]
  | smul_left r x y _ _ h => simp [smul_mem _ r h]
  | smul_right r x y _ _ h => simp [smul_mem _ r h]
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x y : L
hx : Membership.mem (γ := Submodule R L) (span R s) x
hy : Membership.mem (γ := Submodule R L) (span R s) y
mem_mem : ∀ (x y : L) (hx : x ∈ s) (hy : y ∈ s), Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
zero_left :
  ∀ (y : L) (hy : Membership.mem (γ := Submodule R L) (span R s) y),
    Membership.mem (γ := Submodule R L) (span R s) (Bracket.bracket (L := L) 0 y)
zero_right :
  ∀ (x : L) (hx : Membership.mem (γ := Submodule R L) (span R s) x),
    Membership.mem (γ := Submodule R L) (span R s) ⁅x, 0⁆
⊢ Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
have add_left : ∀ (x y z : L),
  Membership.mem (γ := Submodule R L) (span R s) x →
    Membership.mem (γ := Submodule R L) (span R s) y →
      Membership.mem (γ := Submodule R L) (span R s) z →
        ∀ (hx : Membership.mem (γ := Submodule R L) (span R s) ⁅x, z⁆)
          (hy : Membership.mem (γ := Submodule R L) (span R s) ⁅y, z⁆),
          Membership.mem (γ := Submodule R L) (span R s) ⁅x + y, z⁆
Tactic: induction hx, hy using span_induction₂ with
  | mem_mem x y hx hy => simp [hs x hx y hy]
  | zero_left y hy => simp
  | zero_right x hx => simp
  | add_left x y z _ _ _ hx hy => simp [add_mem hx hy]
  | add_right x y z _ _ _ hx hy => simp [add_mem hx hy]
  | smul_left r x y _ _ h => simp [smul_mem _ r h]
  | smul_right r x y _ _ h => simp [smul_mem _ r h]
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x y : L
hx : Membership.mem (γ := Submodule R L) (span R s) x
hy : Membership.mem (γ := Submodule R L) (span R s) y
mem_mem : ∀ (x y : L) (hx : x ∈ s) (hy : y ∈ s), Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
zero_left :
  ∀ (y : L) (hy : Membership.mem (γ := Submodule R L) (span R s) y),
    Membership.mem (γ := Submodule R L) (span R s) (Bracket.bracket (L := L) 0 y)
zero_right :
  ∀ (x : L) (hx : Membership.mem (γ := Submodule R L) (span R s) x),
    Membership.mem (γ := Submodule R L) (span R s) ⁅x, 0⁆
add_left :
  ∀ (x y z : L),
    Membership.mem (γ := Submodule R L) (span R s) x →
      Membership.mem (γ := Submodule R L) (span R s) y →
        Membership.mem (γ := Submodule R L) (span R s) z →
          ∀ (hx : Membership.mem (γ := Submodule R L) (span R s) ⁅x, z⁆)
            (hy : Membership.mem (γ := Submodule R L) (span R s) ⁅y, z⁆),
            Membership.mem (γ := Submodule R L) (span R s) ⁅x + y, z⁆
⊢ Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
have add_right : ∀ (x y z : L),
  Membership.mem (γ := Submodule R L) (span R s) x →
    Membership.mem (γ := Submodule R L) (span R s) y →
      Membership.mem (γ := Submodule R L) (span R s) z →
        ∀ (hx : Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆)
          (hy : Membership.mem (γ := Submodule R L) (span R s) ⁅x, z⁆),
          Membership.mem (γ := Submodule R L) (span R s) ⁅x, y + z⁆
Tactic: induction hx, hy using span_induction₂ with
  | mem_mem x y hx hy => simp [hs x hx y hy]
  | zero_left y hy => simp
  | zero_right x hx => simp
  | add_left x y z _ _ _ hx hy => simp [add_mem hx hy]
  | add_right x y z _ _ _ hx hy => simp [add_mem hx hy]
  | smul_left r x y _ _ h => simp [smul_mem _ r h]
  | smul_right r x y _ _ h => simp [smul_mem _ r h]
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x y : L
hx : Membership.mem (γ := Submodule R L) (span R s) x
hy : Membership.mem (γ := Submodule R L) (span R s) y
mem_mem : ∀ (x y : L) (hx : x ∈ s) (hy : y ∈ s), Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
zero_left :
  ∀ (y : L) (hy : Membership.mem (γ := Submodule R L) (span R s) y),
    Membership.mem (γ := Submodule R L) (span R s) (Bracket.bracket (L := L) 0 y)
zero_right :
  ∀ (x : L) (hx : Membership.mem (γ := Submodule R L) (span R s) x),
    Membership.mem (γ := Submodule R L) (span R s) ⁅x, 0⁆
add_left :
  ∀ (x y z : L),
    Membership.mem (γ := Submodule R L) (span R s) x →
      Membership.mem (γ := Submodule R L) (span R s) y →
        Membership.mem (γ := Submodule R L) (span R s) z →
          ∀ (hx : Membership.mem (γ := Submodule R L) (span R s) ⁅x, z⁆)
            (hy : Membership.mem (γ := Submodule R L) (span R s) ⁅y, z⁆),
            Membership.mem (γ := Submodule R L) (span R s) ⁅x + y, z⁆
add_right :
  ∀ (x y z : L),
    Membership.mem (γ := Submodule R L) (span R s) x →
      Membership.mem (γ := Submodule R L) (span R s) y →
        Membership.mem (γ := Submodule R L) (span R s) z →
          ∀ (hx : Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆)
            (hy : Membership.mem (γ := Submodule R L) (span R s) ⁅x, z⁆),
            Membership.mem (γ := Submodule R L) (span R s) ⁅x, y + z⁆
⊢ Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
have smul_left : ∀ (r : R) (x y : L),
  Membership.mem (γ := Submodule R L) (span R s) x →
    Membership.mem (γ := Submodule R L) (span R s) y →
      ∀ (h : Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆),
        Membership.mem (γ := Submodule R L) (span R s) ⁅r • x, y⁆
Tactic: induction hx, hy using span_induction₂ with
  | mem_mem x y hx hy => simp [hs x hx y hy]
  | zero_left y hy => simp
  | zero_right x hx => simp
  | add_left x y z _ _ _ hx hy => simp [add_mem hx hy]
  | add_right x y z _ _ _ hx hy => simp [add_mem hx hy]
  | smul_left r x y _ _ h => simp [smul_mem _ r h]
  | smul_right r x y _ _ h => simp [smul_mem _ r h]
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x y : L
hx : Membership.mem (γ := Submodule R L) (span R s) x
hy : Membership.mem (γ := Submodule R L) (span R s) y
mem_mem : ∀ (x y : L) (hx : x ∈ s) (hy : y ∈ s), Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
zero_left :
  ∀ (y : L) (hy : Membership.mem (γ := Submodule R L) (span R s) y),
    Membership.mem (γ := Submodule R L) (span R s) (Bracket.bracket (L := L) 0 y)
zero_right :
  ∀ (x : L) (hx : Membership.mem (γ := Submodule R L) (span R s) x),
    Membership.mem (γ := Submodule R L) (span R s) ⁅x, 0⁆
add_left :
  ∀ (x y z : L),
    Membership.mem (γ := Submodule R L) (span R s) x →
      Membership.mem (γ := Submodule R L) (span R s) y →
        Membership.mem (γ := Submodule R L) (span R s) z →
          ∀ (hx : Membership.mem (γ := Submodule R L) (span R s) ⁅x, z⁆)
            (hy : Membership.mem (γ := Submodule R L) (span R s) ⁅y, z⁆),
            Membership.mem (γ := Submodule R L) (span R s) ⁅x + y, z⁆
add_right :
  ∀ (x y z : L),
    Membership.mem (γ := Submodule R L) (span R s) x →
      Membership.mem (γ := Submodule R L) (span R s) y →
        Membership.mem (γ := Submodule R L) (span R s) z →
          ∀ (hx : Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆)
            (hy : Membership.mem (γ := Submodule R L) (span R s) ⁅x, z⁆),
            Membership.mem (γ := Submodule R L) (span R s) ⁅x, y + z⁆
smul_left :
  ∀ (r : R) (x y : L),
    Membership.mem (γ := Submodule R L) (span R s) x →
      Membership.mem (γ := Submodule R L) (span R s) y →
        ∀ (h : Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆),
          Membership.mem (γ := Submodule R L) (span R s) ⁅r • x, y⁆
⊢ Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆
have smul_right : ∀ (r : R) (x y : L),
  Membership.mem (γ := Submodule R L) (span R s) x →
    Membership.mem (γ := Submodule R L) (span R s) y →
      ∀ (h : Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆),
        Membership.mem (γ := Submodule R L) (span R s) ⁅x, r • y⁆
Tactic: induction hx, hy using span_induction₂ with
  | mem_mem x y hx hy => simp [hs x hx y hy]
  | zero_left y hy => simp
  | zero_right x hx => simp
  | add_left x y z _ _ _ hx hy => simp [add_mem hx hy]
  | add_right x y z _ _ _ hx hy => simp [add_mem hx hy]
  | smul_left r x y _ _ h => simp [smul_mem _ r h]
  | smul_right r x y _ _ h => simp [smul_mem _ r h]
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
⊢ Eq (α := LieSubalgebra R L) (lieSpan R L (-s)) (lieSpan R L s)
have suffices : ∀ (s : Set L), LE.le (α := LieSubalgebra R L) (lieSpan R L (-s)) (lieSpan R L s)
Tactic: suffices ∀ s : Set L, lieSpan R L (-s) ≤ lieSpan R L s from
    le_antisymm (this s) <| by simpa using (this (-s))
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s_1 s : Set L
x : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x
have mem : ∀ (y : L) (h : y ∈ -s), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
Tactic: induction hx using lieSpan_induction with
  | mem y h => exact neg_mem_iff.mp <| subset_lieSpan <| Set.mem_neg.mp h
  | zero => exact zero_mem _
  | add _ _ _ _ hu hv => exact add_mem hu hv
  | smul t _ _ hu => exact SMulMemClass.smul_mem t hu
  | lie _ _ _ _ hu hv => exact lie_mem _ hu hv
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s_1 s : Set L
x : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x
mem : ∀ (y : L) (h : y ∈ -s), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x
have zero : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) 0
Tactic: induction hx using lieSpan_induction with
  | mem y h => exact neg_mem_iff.mp <| subset_lieSpan <| Set.mem_neg.mp h
  | zero => exact zero_mem _
  | add _ _ _ _ hu hv => exact add_mem hu hv
  | smul t _ _ hu => exact SMulMemClass.smul_mem t hu
  | lie _ _ _ _ hu hv => exact lie_mem _ hu hv
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s_1 s : Set L
x : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x
mem : ∀ (y : L) (h : y ∈ -s), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
zero : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) 0
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x
have add : ∀ (x y : L),
  Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x →
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) y →
      ∀ (hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x)
        (hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y),
        Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) (x + y)
Tactic: induction hx using lieSpan_induction with
  | mem y h => exact neg_mem_iff.mp <| subset_lieSpan <| Set.mem_neg.mp h
  | zero => exact zero_mem _
  | add _ _ _ _ hu hv => exact add_mem hu hv
  | smul t _ _ hu => exact SMulMemClass.smul_mem t hu
  | lie _ _ _ _ hu hv => exact lie_mem _ hu hv
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s_1 s : Set L
x : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x
mem : ∀ (y : L) (h : y ∈ -s), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
zero : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) 0
add :
  ∀ (x y : L),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x →
      Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) y →
        ∀ (hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x)
          (hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y),
          Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) (x + y)
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x
have smul : ∀ (t : R) (x : L),
  Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x →
    ∀ (hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x),
      Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) (t • x)
Tactic: induction hx using lieSpan_induction with
  | mem y h => exact neg_mem_iff.mp <| subset_lieSpan <| Set.mem_neg.mp h
  | zero => exact zero_mem _
  | add _ _ _ _ hu hv => exact add_mem hu hv
  | smul t _ _ hu => exact SMulMemClass.smul_mem t hu
  | lie _ _ _ _ hu hv => exact lie_mem _ hu hv
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s_1 s : Set L
x : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x
mem : ∀ (y : L) (h : y ∈ -s), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
zero : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) 0
add :
  ∀ (x y : L),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x →
      Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) y →
        ∀ (hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x)
          (hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y),
          Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) (x + y)
smul :
  ∀ (t : R) (x : L),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x →
      ∀ (hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x),
        Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) (t • x)
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x
have lie : ∀ (x y : L),
  Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x →
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) y →
      ∀ (hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x)
        (hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y),
        Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) ⁅x, y⁆
Tactic: induction hx using lieSpan_induction with
  | mem y h => exact neg_mem_iff.mp <| subset_lieSpan <| Set.mem_neg.mp h
  | zero => exact zero_mem _
  | add _ _ _ _ hu hv => exact add_mem hu hv
  | smul t _ _ hu => exact SMulMemClass.smul_mem t hu
  | lie _ _ _ _ hu hv => exact lie_mem _ hu hv
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
⊢ Eq (α := LieSubalgebra R ↥(lieSpan R L s))
    (lieSpan R (↥(lieSpan R L s))
      (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
    ⊤
have rw : LE.le (α := LieSubalgebra R ↥(lieSpan R L s)) ⊤
  (lieSpan R (↥(lieSpan R L s))
    (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
x 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 :
  Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
    (lieSpan R (↥(lieSpan R L s))
      (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
    (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u hx)
hv :
  Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
    (lieSpan R (↥(lieSpan R L s))
      (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
    (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) v hy)
⊢ Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
    (lieSpan R (↥(lieSpan R L s))
      (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
    (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) (u + v) ⋯)
have add : ∀
  (hu :
    Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
      (lieSpan R (↥(lieSpan R L s))
        (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u hx))
  (hv :
    Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
      (lieSpan R (↥(lieSpan R L s))
        (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) v hy)),
  Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
    (lieSpan R (↥(lieSpan R L s))
      (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
    (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) (u + v) sorry)
Tactic: revert hu hv
Cleared hypotheses: hu, hv
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
x : L
t : R
u : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) u
hu :
  Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
    (lieSpan R (↥(lieSpan R L s))
      (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
    (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u hx)
⊢ Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
    (lieSpan R (↥(lieSpan R L s))
      (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
    (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) (t • u) ⋯)
have smul : ∀
  (hu :
    Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
      (lieSpan R (↥(lieSpan R L s))
        (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) u hx)),
  Membership.mem (γ := LieSubalgebra R ↥(lieSpan R L s))
    (lieSpan R (↥(lieSpan R L s))
      (Subtype.val (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) ⁻¹' s))
    (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x) (t • u) sorry)
Tactic: revert hu
Cleared hypotheses: hu