awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
p_1 : (x : L) → Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x → Prop
mem : ∀ (x : L) (h : x ∈ s), p_1 x ⋯
zero : p_1 0 ⋯
add :
  ∀ (x y : L) (hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x)
    (hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y), p_1 x hx → p_1 y hy → p_1 (x + y) ⋯
smul : ∀ (a : R) (x : L) (hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x), p_1 x hx → p_1 (a • x) ⋯
x : L
lie :
  ∀ (x y : L) (hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x)
    (hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y), p_1 x hx → p_1 y hy → p_1 ⁅x, y⁆ ⋯
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x
p : LieSubalgebra R L :=
  { carrier := {x : L | ∃ (hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x), p_1 x hx}, add_mem' := ⋯,
    zero_mem' := ⋯, smul_mem' := ⋯, lie_mem' := ⋯ }
⊢ p_1 x hx

Tactic:
lieSpan_le (K := p) |>.mpr (fun y hy ↦ ⟨subset_lieSpan hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Premises used: Iff.mpr, id, LieSubalgebra.subset_lieSpan, Exists.intro, LieSubalgebra.lieSpan_le, Exists.elim
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
p_1 : (x : L) → Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x → Prop
mem : ∀ (x : L) (h : x ∈ s), p_1 x ⋯
zero : p_1 0 ⋯
add :
  ∀ (x y : L) (hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x)
    (hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y), p_1 x hx → p_1 y hy → p_1 (x + y) ⋯
smul : ∀ (a : R) (x : L) (hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x), p_1 x hx → p_1 (a • x) ⋯
x : L
lie :
  ∀ (x y : L) (hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x)
    (hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y), p_1 x hx → p_1 y hy → p_1 ⁅x, y⁆ ⋯
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x
p : LieSubalgebra R L :=
  { carrier := {x : L | ∃ (hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x), p_1 x hx}, add_mem' := ⋯,
    zero_mem' := ⋯, smul_mem' := ⋯, lie_mem' := ⋯ }
⊢ p_1 x hx

Tactic:
exact lieSpan_le (K := p) |>.mpr (fun y hy ↦ ⟨subset_lieSpan hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Premises used: Iff.mpr, LieSubalgebra.subset_lieSpan, Exists.intro, LieSubalgebra.lieSpan_le, Exists.elim
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
this : ∀ (s : Set L), LE.le (α := LieSubalgebra R L) (lieSpan R L (-s)) (lieSpan R L s)
⊢ LE.le (α := LieSubalgebra R L) (lieSpan R L s) (lieSpan R L (-s))

Tactic:
simpa using (this (-s))

Premises used: Neg.neg
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
suffices : ∀ (s : Set L), LE.le (α := LieSubalgebra R L) (lieSpan R L (-s)) (lieSpan R L s)
⊢ Eq (α := 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))
-- Module: Mathlib.Algebra.Lie.Subalgebra
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 y : L
h : y ∈ -s
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y

Tactic:
neg_mem_iff.mp <| subset_lieSpan <| Set.mem_neg.mp h

Premises used: Set.mem_neg, neg_mem_iff, LieSubalgebra.subset_lieSpan, Iff.mp
-- Module: Mathlib.Algebra.Lie.Subalgebra
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 y : L
h : y ∈ -s
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y

Tactic:
exact neg_mem_iff.mp <| subset_lieSpan <| Set.mem_neg.mp h

Premises used: Set.mem_neg, neg_mem_iff, LieSubalgebra.subset_lieSpan, Iff.mp
-- Module: Mathlib.Algebra.Lie.Subalgebra
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
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
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
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
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 x_1 y : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x_1
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) y
hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x_1
hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) (x_1 + y)

Tactic:
add_mem hu hv

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
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 x_1 y : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x_1
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) y
hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x_1
hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) (x_1 + y)

Tactic:
exact add_mem hu hv

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
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
t : R
x_1 : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x_1
hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x_1
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) (t • x_1)

Tactic:
SMulMemClass.smul_mem t hu

Premises used: SMulMemClass.smul_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
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
t : R
x_1 : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x_1
hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x_1
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) (t • x_1)

Tactic:
exact SMulMemClass.smul_mem t hu

Premises used: SMulMemClass.smul_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
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 x_1 y : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x_1
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) y
hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x_1
hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) ⁅x_1, y⁆

Tactic:
lie_mem _ hu hv

Premises used: LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
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 x_1 y : L
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) x_1
hy : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (-s)) y
hu : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x_1
hv : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) y
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) ⁅x_1, y⁆

Tactic:
exact lie_mem _ hu hv

Premises used: LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
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)
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⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) 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

Premises used: neg_mem_iff, LieSubalgebra.subset_lieSpan, Iff.mp, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
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))
⊢ 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))
    ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
x u : L
hu : u ∈ s
⊢ Membership.mem (γ := Set ↥(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 ⋯)

Tactic:
simpa
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
x u : L
hu : u ∈ s
⊢ 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 ⋯)

Tactic:
exact subset_lieSpan <| by simpa

Premises used: LieSubalgebra.subset_lieSpan
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
x : L
⊢ 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) 0 ⋯)

Tactic:
zero_mem _

Premises used: Set.Mem, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
s : Set L
x : L
⊢ 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) 0 ⋯)

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
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)
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) ⋯)
⊢ 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) ⋯)

Tactic:
revert hu hv
-- Module: Mathlib.Algebra.Lie.Subalgebra
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) ⋯)

Tactic:
add_mem

Premises used: Set.Mem, AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
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) ⋯)

Tactic:
exact add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
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)
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) ⋯)
⊢ 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) ⋯)

Tactic:
revert hu
-- Module: Mathlib.Algebra.Lie.Subalgebra
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) ⋯)

Tactic:
LieSubalgebra.smul_mem _ _

Premises used: Set.Mem, LieSubalgebra.smul_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
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) ⋯)

Tactic:
exact LieSubalgebra.smul_mem _ _

Premises used: LieSubalgebra.smul_mem
-- Module: Mathlib.Algebra.Lie.Subalgebra
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)
lie :
  ∀
    (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⁆ ⋯)
⊢ 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⁆ ⋯)

Tactic:
revert hu hv
-- Module: Mathlib.Algebra.Lie.Subalgebra
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⁆ ⋯)

Tactic:
LieSubalgebra.lie_mem _

Premises used: Set.Mem, LieSubalgebra.lie_mem