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
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
h₁ : (↑x : L) ∈ K ↔ x ∈ comap K'.incl K
⊢ x ∈ ofLe h ↔ x ∈ comap K'.incl K

Tactic:
rw [mem_ofLe]

Premises used: LieSubalgebra.mem_ofLe
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ (↑x : L) ∈ K ↔ x ∈ comap K'.incl K

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (ofLe h).toSubmodule = (Submodule.inclusion h).range

Tactic:
rfl

Premises used: Set.Mem, LinearMap.range, rfl, Submodule.copy
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K
⊢ Eq (α := ↥(ofLe h)) ((equivOfLe h : (a : ↥K) → ↥(ofLe h)) x : ↥(ofLe h))
    (Subtype.mk (p := fun (x : ↥K') ↦ x ∈ ofLe h) ((inclusion h : (a : ↥K) → ↥K') x) ⋯ : ↥(ofLe h))

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K : LieSubalgebra R L
K' : LieSubalgebra R L₂
⊢ map f K ≤ K' ↔ K ≤ comap f K'

Tactic:
Set.image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_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
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
⊢ GaloisConnection (map f) (comap f)

Tactic:
fun _ _ ↦ map_le_iff_le_comap

Premises used: LieSubalgebra.map_le_iff_le_comap, GaloisConnection
-- 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
rw :
  Membership.mem (γ := Set L)
      (⋂ (s_1 : LieSubalgebra R L),
        ⋂ (_ : Membership.mem (γ := Set (LieSubalgebra R L)) {N : LieSubalgebra R L | s ⊆ (↑N : Set L)} s_1),
          (↑s_1 : Set L))
      x ↔
    ∀ (K : LieSubalgebra R L), s ⊆ (↑K : Set L) → x ∈ K
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x ↔ ∀ (K : LieSubalgebra R L), s ⊆ (↑K : Set L) → x ∈ K

Tactic:
rw [← SetLike.mem_coe, lieSpan, coe_sInf]

Premises used: LieSubalgebra.coe_sInf, LieSubalgebra.lieSpan, SetLike.mem_coe
-- 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 (γ := Set L)
      (⋂ (s_1 : LieSubalgebra R L),
        ⋂ (_ : Membership.mem (γ := Set (LieSubalgebra R L)) {N : LieSubalgebra R L | s ⊆ (↑N : Set L)} s_1),
          (↑s_1 : Set L))
      x ↔
    ∀ (K : LieSubalgebra R L), s ⊆ (↑K : Set L) → x ∈ K

Tactic:
Set.mem_iInter₂

Premises used: Set.Mem, setOf, Set.mem_iInter₂
-- 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 (γ := Set L)
      (⋂ (s_1 : LieSubalgebra R L),
        ⋂ (_ : Membership.mem (γ := Set (LieSubalgebra R L)) {N : LieSubalgebra R L | s ⊆ (↑N : Set L)} s_1),
          (↑s_1 : Set L))
      x ↔
    ∀ (K : LieSubalgebra R L), s ⊆ (↑K : Set L) → x ∈ K

Tactic:
exact Set.mem_iInter₂

Premises used: Set.mem_iInter₂
-- 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
m : L
hm : m ∈ s
rw : ∀ (K : LieSubalgebra R L), s ⊆ (↑K : Set L) → m ∈ K
⊢ m ∈ (↑(lieSpan R L s) : Set L)

Tactic:
rw [SetLike.mem_coe, mem_lieSpan]

Premises used: SetLike.mem_coe, LieSubalgebra.mem_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
m : L
hm : m ∈ s
K : LieSubalgebra R L
hK : s ⊆ (↑K : Set L)
⊢ m ∈ K

Tactic:
hK hm
-- 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
m : L
hm : m ∈ s
K : LieSubalgebra R L
hK : s ⊆ (↑K : Set L)
⊢ m ∈ K

Tactic:
exact hK hm
-- 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 : s ⊆ (↑(lieSpan R L s) : Set L)
⊢ LE.le (α := Submodule R L) (Submodule.span R s) (toSubmodule (lieSpan R L s))

Tactic:
rw [Submodule.span_le, coe_toSubmodule]

Premises used: LieSubalgebra.coe_toSubmodule, Submodule.span_le
-- 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
⊢ s ⊆ (↑(lieSpan R L s) : Set L)

Tactic:
apply subset_lieSpan

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
K : LieSubalgebra R L
mp : lieSpan R L s ≤ K → s ⊆ (↑K : Set L)
mpr : s ⊆ (↑K : Set L) → lieSpan R L s ≤ K
⊢ lieSpan R L s ≤ K ↔ s ⊆ (↑K : Set L)

Tactic:
constructor
-- 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
K : LieSubalgebra R L
⊢ lieSpan R L s ≤ K → s ⊆ (↑K : Set L)

Tactic:
Set.Subset.trans subset_lieSpan

Premises used: Set.Subset.trans, LieSubalgebra.subset_lieSpan, Set.Subset
-- 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
K : LieSubalgebra R L
⊢ lieSpan R L s ≤ K → s ⊆ (↑K : Set L)

Tactic:
exact Set.Subset.trans subset_lieSpan

Premises used: Set.Subset.trans, 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
K : LieSubalgebra R L
hs : s ⊆ (↑K : Set L)
m : L
hm : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) m
⊢ ∀ (K : LieSubalgebra R L), s ⊆ (↑K : Set L) → m ∈ K

Tactic:
rw [mem_lieSpan] at hm

Premises used: LieSubalgebra.mem_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
K : LieSubalgebra R L
hs : s ⊆ (↑K : Set L)
m : L
hm : ∀ (K : LieSubalgebra R L), s ⊆ (↑K : Set L) → m ∈ K
⊢ m ∈ K

Tactic:
hm _ hs
-- 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
K : LieSubalgebra R L
hs : s ⊆ (↑K : Set L)
m : L
hm : ∀ (K : LieSubalgebra R L), s ⊆ (↑K : Set L) → m ∈ K
⊢ m ∈ K

Tactic:
exact hm _ hs
-- 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 t : Set L
h : s ⊆ t
rw : s ⊆ (↑(lieSpan R L t) : Set L)
⊢ LE.le (α := LieSubalgebra R L) (lieSpan R L s) (lieSpan R L t)

Tactic:
rw [lieSpan_le]

Premises used: LieSubalgebra.lieSpan_le
-- 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 t : Set L
h : s ⊆ t
⊢ s ⊆ (↑(lieSpan R L t) : Set L)

Tactic:
Set.Subset.trans h subset_lieSpan

Premises used: Set.Subset.trans, 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 t : Set L
h : s ⊆ t
⊢ s ⊆ (↑(lieSpan R L t) : Set L)

Tactic:
exact Set.Subset.trans h subset_lieSpan

Premises used: Set.Subset.trans, 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
K : LieSubalgebra R L
⊢ lieSpan R L (↑K : Set L) = K

Tactic:
le_antisymm (lieSpan_le.mpr rfl.subset) subset_lieSpan

Premises used: Iff.mpr, LieSubalgebra.subset_lieSpan, Eq.subset, le_antisymm, LieSubalgebra.lieSpan_le, rfl
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
p : Submodule R L
rw : toSubmodule (lieSpan R L (↑p : Set L)) = p ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ toSubmodule (lieSpan R L (↑p : Set L)) = p ↔ ∃ (K : LieSubalgebra R L), K.toSubmodule = p

Tactic:
rw [p.exists_lieSubalgebra_coe_eq_iff]

Premises used: Submodule.exists_lieSubalgebra_coe_eq_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
p : Submodule R L
mp : toSubmodule (lieSpan R L (↑p : Set L)) = p → ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
mpr : (∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p) → toSubmodule (lieSpan R L (↑p : Set L)) = p
⊢ toSubmodule (lieSpan R L (↑p : Set L)) = p ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
p : Submodule R L
h : toSubmodule (lieSpan R L (↑p : Set L)) = p
x m : L
hm : x ∈ p
mp :
  Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (↑p : Set L)) m →
    Membership.mem (γ := Submodule R L) (toSubmodule (lieSpan R L (↑p : Set L))) ⁅x, m⁆
⊢ m ∈ p → ⁅x, m⁆ ∈ p

Tactic:
rw [← h, mem_toSubmodule]

Premises used: LieSubalgebra.mem_toSubmodule
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
p : Submodule R L
h : toSubmodule (lieSpan R L (↑p : Set L)) = p
x m : L
hm : x ∈ p
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (↑p : Set L)) m →
    Membership.mem (γ := Submodule R L) (toSubmodule (lieSpan R L (↑p : Set L))) ⁅x, m⁆

Tactic:
lie_mem _ (subset_lieSpan hm)

Premises used: Set.Mem, LieSubalgebra.subset_lieSpan, 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
p : Submodule R L
h : toSubmodule (lieSpan R L (↑p : Set L)) = p
x m : L
hm : x ∈ p
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (↑p : Set L)) m →
    Membership.mem (γ := Submodule R L) (toSubmodule (lieSpan R L (↑p : Set L))) ⁅x, m⁆

Tactic:
exact lie_mem _ (subset_lieSpan hm)

Premises used: LieSubalgebra.subset_lieSpan, 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
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
mpr :
  toSubmodule (lieSpan R L (↑{ toSubmodule := p, lie_mem' := h : LieSubalgebra R L }.toSubmodule : Set L)) =
    { toSubmodule := p, lie_mem' := h : LieSubalgebra R L }.toSubmodule
mpr₁ :
  toSubmodule (lieSpan R L (↑{ toSubmodule := p, lie_mem' := h : LieSubalgebra R L } : Set L)) =
    { toSubmodule := p, lie_mem' := h : LieSubalgebra R L }.toSubmodule
mpr₂ :
  lieSpan R L (↑{ toSubmodule := p, lie_mem' := h : LieSubalgebra R L } : Set L) =
    { toSubmodule := p, lie_mem' := h : LieSubalgebra R L }
mpr₃ mpr₄ : { toSubmodule := p, lie_mem' := h : LieSubalgebra R L } = { toSubmodule := p, lie_mem' := h }
⊢ toSubmodule (lieSpan R L (↑p : Set L)) = p

Tactic:
rw [← toSubmodule_mk p @h, coe_toSubmodule, toSubmodule_inj, lieSpan_eq]

Premises used: LieSubalgebra.coe_toSubmodule, LieSubalgebra.toSubmodule_inj, LieSubalgebra.toSubmodule_mk, LieSubalgebra.lieSpan_eq
-- 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
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)

Tactic:
le_antisymm ?_ submodule_span_le_lieSpan

Premises used: LieSubalgebra.submodule_span_le_lieSpan, le_antisymm
-- 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
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⁆
refine : LE.le (α := Submodule R L) (toSubmodule (lieSpan R L s)) (span R s)
⊢ Eq (α := Submodule R L) (toSubmodule (lieSpan R L s)) (span R s)

Tactic:
refine le_antisymm ?_ submodule_span_le_lieSpan

Premises used: LieSubalgebra.submodule_span_le_lieSpan, le_antisymm
-- 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
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⁆
rw :
  s ⊆
    (↑(let __src : Submodule R L := span R s;
        { toSubmodule := __src, lie_mem' := ⋯ }) :
      Set L)
⊢ LE.le (α := LieSubalgebra R L) (lieSpan R L s)
    (let __src : Submodule R L := span R s;
    { toSubmodule := __src, lie_mem' := ⋯ })

Tactic:
rw [lieSpan_le]

Premises used: LieSubalgebra.lieSpan_le
-- 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
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⁆
⊢ s ⊆
    (↑(let __src : Submodule R L := span R s;
        { toSubmodule := __src, lie_mem' := ⋯ }) :
      Set L)

Tactic:
subset_span

Premises used: Submodule.subset_span
-- 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
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⁆
⊢ s ⊆
    (↑(let __src : Submodule R L := span R s;
        { toSubmodule := __src, lie_mem' := ⋯ }) :
      Set L)

Tactic:
exact subset_span

Premises used: Submodule.subset_span
-- 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
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
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⁆
⊢ Eq (α := Submodule R L) (toSubmodule (lieSpan R L s)) (span R s)

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
-- 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
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 y_1 x y : L
hx : x ∈ s
hy : y ∈ s
⊢ Membership.mem (γ := Submodule R L) (span R s) ⁅x, y⁆

Tactic:
simp [hs x hx y hy]
-- 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
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x y_1 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:
simp
-- 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
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 y x : L
hx : Membership.mem (γ := Submodule R L) (span R s) x
⊢ Membership.mem (γ := Submodule R L) (span R s) ⁅x, 0⁆

Tactic:
simp
-- 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
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 y_1 x y z : L
hx_1 : Membership.mem (γ := Submodule R L) (span R s) x
hy_1 : Membership.mem (γ := Submodule R L) (span R s) y
hz : 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:
simp [add_mem hx hy]

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
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 y_1 x y z : L
hx_1 : Membership.mem (γ := Submodule R L) (span R s) x
hy_1 : Membership.mem (γ := Submodule R L) (span R s) y
hz : 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:
simp [add_mem hx hy]

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
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 y_1 : L
r : R
x y : L
hx : Membership.mem (γ := Submodule R L) (span R s) x
hy : 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:
simp [smul_mem _ r h]

Premises used: Submodule.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
hs : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x_1 y_1 : L
r : R
x y : L
hx : Membership.mem (γ := Submodule R L) (span R s) x
hy : 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:
simp [smul_mem _ r h]

Premises used: Submodule.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
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⁆
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⁆
⊢ 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]

Premises used: Submodule.span_induction₂, 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
⊢ Eq (α := LieSubalgebra R L) (lieSpan R L ∅) ⊥

Tactic:
(LieSubalgebra.gi R L).gc.l_bot

Premises used: LieSubalgebra.gi, GaloisConnection.l_bot, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ Eq (α := LieSubalgebra R L) (lieSpan R L univ) ⊤

Tactic:
eq_top_iff.2 <| SetLike.le_def.2 <| subset_lieSpan

Premises used: Iff.mpr, eq_top_iff, SetLike.le_def, 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 t : Set L
⊢ Eq (α := LieSubalgebra R L) (lieSpan R L (s ∪ t)) (lieSpan R L s ⊔ lieSpan R L t)

Tactic:
(LieSubalgebra.gi R L).gc.l_sup

Premises used: LieSubalgebra.gi, GaloisConnection.l_sup, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
ι : Sort u_1
s : ι → Set L
⊢ Eq (α := LieSubalgebra R L) (lieSpan R L (⋃ (i : ι), s i)) (⨆ (i : ι), lieSpan R L (s i))

Tactic:
(LieSubalgebra.gi R L).gc.l_iSup

Premises used: LieSubalgebra.gi, GaloisConnection.l_iSup, Set.iUnion, GaloisInsertion.gc
-- 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 : (x : L) → Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x → Prop
mem : ∀ (x : L) (h : x ∈ s), p x ⋯
zero : p 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 x hx → p y hy → p (x + y) ⋯
smul : ∀ (a : R) (x : L) (hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x), p x hx → p (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 x hx → p y hy → p ⁅x, y⁆ ⋯
hx : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x
let : p x hx
⊢ p x hx

Tactic:
let p : LieSubalgebra R L :=
    { carrier := { x | ∃ hx, p x hx }
      add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
      zero_mem' := ⟨_, zero⟩
      smul_mem' := fun r ↦ fun ⟨_, hpx⟩ ↦ ⟨_, smul r _ _ hpx⟩
      lie_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, lie _ _ _ _ hpx hpy⟩ }