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
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
K : LieSubalgebra R L
e : L ≃ₗ⁅R⁆ L₂
x : L₂
⊢ x ∈ map e.toLieHom K ↔ x ∈ Submodule.map (↑e.toLinearEquiv : L →ₗ[R] L₂) K.toSubmodule

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.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 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x y : L
hx : x ∈ (Submodule.comap (↑f : L →ₗ[R] L₂) K₂.toSubmodule).carrier
hy : y ∈ (Submodule.comap (↑f : L →ₗ[R] L₂) K₂.toSubmodule).carrier
this : Membership.mem (α := L₂) K₂ (Bracket.bracket (L := L₂) ((f : (a : L) → L₂) x : L₂) ((f : (a : L) → L₂) y) : L₂)
⊢ ⁅x, y⁆ ∈ (Submodule.comap (↑f : L →ₗ[R] L₂) K₂.toSubmodule).carrier

Tactic:
simp [this]
-- 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 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x y : L
hx : x ∈ (Submodule.comap (↑f : L →ₗ[R] L₂) K₂.toSubmodule).carrier
hy : y ∈ (Submodule.comap (↑f : L →ₗ[R] L₂) K₂.toSubmodule).carrier
suffices :
  Membership.mem (α := L₂) K₂ (Bracket.bracket (L := L₂) ((f : (a : L) → L₂) x : L₂) ((f : (a : L) → L₂) y) : L₂)
⊢ ⁅x, y⁆ ∈ (Submodule.comap (↑f : L →ₗ[R] L₂) K₂.toSubmodule).carrier

Tactic:
suffices ⁅f x, f y⁆ ∈ K₂ by simp [this]
-- 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 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x y : L
hx : x ∈ (Submodule.comap (↑f : L →ₗ[R] L₂) K₂.toSubmodule).carrier
hy : y ∈ (Submodule.comap (↑f : L →ₗ[R] L₂) K₂.toSubmodule).carrier
⊢ Membership.mem (α := L₂) K₂ (Bracket.bracket (L := L₂) ((f : (a : L) → L₂) x : L₂) ((f : (a : L) → L₂) y) : L₂)

Tactic:
K₂.lie_mem hx hy

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
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x y : L
hx : x ∈ (Submodule.comap (↑f : L →ₗ[R] L₂) K₂.toSubmodule).carrier
hy : y ∈ (Submodule.comap (↑f : L →ₗ[R] L₂) K₂.toSubmodule).carrier
⊢ Membership.mem (α := L₂) K₂ (Bracket.bracket (L := L₂) ((f : (a : L) → L₂) x : L₂) ((f : (a : L) → L₂) y) : L₂)

Tactic:
exact K₂.lie_mem hx hy

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
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K₂ : LieSubalgebra R L₂
x : L
⊢ x ∈ comap f K₂ ↔ Membership.mem (α := L₂) K₂ ((f : (a : L) → L₂) x : L₂)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- 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
⊢ K ≤ K' ↔ (↑K : Set L) ⊆ (↑K' : Set L)

Tactic:
Iff.rfl

Premises used: Iff.rfl, 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
K K' : LieSubalgebra R L
⊢ K.toSubmodule ≤ K'.toSubmodule ↔ K ≤ K'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.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
⊢ (↑⊥ : Set L) = {0}

Tactic:
rfl

Premises used: setOf, Set.singleton, 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
⊢ Eq.{v + 1} (α := Submodule R L) (toSubmodule ⊥) ⊥

Tactic:
rfl

Premises used: 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 : LieSubalgebra R L
⊢ K.toSubmodule = ⊥ ↔ K = ⊥

Tactic:
simp [← toSubmodule_inj]

Premises used: LieSubalgebra.toSubmodule_inj
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
⊢ Membership.mem (γ := LieSubalgebra R L) ⊥ x ↔ x = 0

Tactic:
mem_singleton_iff

Premises used: Set.Mem, setOf, Set.mem_singleton_iff, Set.singleton
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ (↑⊤ : Set L) = univ

Tactic:
rfl

Premises used: Set.univ, setOf, 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
⊢ Eq.{v + 1} (α := Submodule R L) (toSubmodule ⊤) ⊤

Tactic:
rfl

Premises used: 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 : LieSubalgebra R L
⊢ K.toSubmodule = ⊤ ↔ K = ⊤

Tactic:
simp [← toSubmodule_inj]

Premises used: LieSubalgebra.toSubmodule_inj
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
⊢ Membership.mem (γ := LieSubalgebra R L) ⊤ x

Tactic:
mem_univ x

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- 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₂
h : ∀ (x : L₂), x ∈ f.range ↔ x ∈ map f ⊤
⊢ f.range = map f ⊤

Tactic:
ext
-- 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₂
x : L₂
⊢ x ∈ f.range ↔ x ∈ map f ⊤

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
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
x y : L
hx :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, v} (R := R) (sInf {x : Submodule R L | ∃ s ∈ S, s.toSubmodule = x}))))
    x
hy :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, v} (R := R) (sInf {x : Submodule R L | ∃ s ∈ S, s.toSubmodule = x}))))
    y
simp :
  ∀ (hx : ∀ a ∈ S, x ∈ (↑a.toSubmodule : Set L)) (hy : ∀ a ∈ S, y ∈ (↑a.toSubmodule : Set L)),
    ∀ a ∈ S, ⁅x, y⁆ ∈ (↑a.toSubmodule : Set L)
⊢ Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, v} (R := R) (sInf {x : Submodule R L | ∃ s ∈ S, s.toSubmodule = x}))))
    ⁅x, y⁆

Tactic:
simp only [Submodule.mem_carrier, mem_iInter, Submodule.coe_sInf, mem_setOf_eq,
          forall_apply_eq_imp_iff₂, exists_imp, and_imp] at hx hy ⊢

Premises used: and_imp, Set.mem_setOf_eq, Set.mem_iInter, Submodule.mem_carrier, exists_imp, forall_apply_eq_imp_iff₂, Submodule.coe_sInf
-- 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_1 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
x y : L
hx : ∀ a ∈ S, x ∈ (↑a.toSubmodule : Set L)
hy : ∀ a ∈ S, y ∈ (↑a.toSubmodule : Set L)
K : LieSubalgebra R L
hK : K ∈ S
⊢ ⁅x, y⁆ ∈ (↑K.toSubmodule : Set L)

Tactic:
K.lie_mem (hx K hK) (hy K hK)

Premises used: Set.Mem, 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
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K_1 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
x y : L
hx : ∀ a ∈ S, x ∈ (↑a.toSubmodule : Set L)
hy : ∀ a ∈ S, y ∈ (↑a.toSubmodule : Set L)
K : LieSubalgebra R L
hK : K ∈ S
⊢ ⁅x, y⁆ ∈ (↑K.toSubmodule : Set L)

Tactic:
exact K.lie_mem (hx K hK) (hy K hK)

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
K K' : LieSubalgebra R L
⊢ (↑(K ⊓ K') : Set L) = (↑K : Set L) ∩ (↑K' : Set L)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, 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
S : Set (LieSubalgebra R L)
⊢ (sInf S).toSubmodule = sInf {x : Submodule R L | ∃ s ∈ S, s.toSubmodule = x}

Tactic:
rfl

Premises used: 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
S : Set (LieSubalgebra R L)
h :
  ∀ (x : L),
    Membership.mem (γ := Set L)
        (⋂ (p : Submodule R L),
          ⋂ (_ : Membership.mem (γ := Set (Submodule R L)) {x : Submodule R L | ∃ s ∈ S, s.toSubmodule = x} p),
            (↑p : Set L))
        x ↔
      Membership.mem (γ := Set L) (⋂ s ∈ S, (↑s : Set L)) x
⊢ Eq.{v + 1} (α := Set L)
    (⋂ (p : Submodule R L),
      ⋂ (_ : Membership.mem (γ := Set (Submodule R L)) {x : Submodule R L | ∃ s ∈ S, s.toSubmodule = x} p),
        (↑p : Set L))
    (⋂ s ∈ S, (↑s : Set L))

Tactic:
ext x
-- 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 (LieSubalgebra R L)
x : L
⊢ Membership.mem (γ := Set L)
      (⋂ (p : Submodule R L),
        ⋂ (_ : Membership.mem (γ := Set (Submodule R L)) {x : Submodule R L | ∃ s ∈ S, s.toSubmodule = x} p),
          (↑p : Set L))
      x ↔
    Membership.mem (γ := Set L) (⋂ s ∈ S, (↑s : Set L)) x

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 (LieSubalgebra R L)
K K' : LieSubalgebra R L
⊢ (↑K : Set L) ≤ (↑K' : Set L) ↔ K ≤ K'

Tactic:
Iff.rfl

Premises used: Iff.rfl, 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 (LieSubalgebra R L)
K K' : LieSubalgebra R L
⊢ (↑K : Set L) ≤ (↑K' : Set L) ↔ K ≤ K'

Tactic:
exact Iff.rfl

Premises used: Iff.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
S : Set (LieSubalgebra R L)
⊢ ∀ (K K' : LieSubalgebra R L), (↑K : Set L) ≤ (↑K' : Set L) ↔ K ≤ K'

Tactic:
have h : ∀ K K' : LieSubalgebra R L, (K : Set L) ≤ K' ↔ K ≤ K' := by
    intros
    exact Iff.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
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), (↑K : Set L) ≤ (↑K' : Set L) ↔ K ≤ K'
apply : IsGLB (SetLike.coe '' S) (↑(sInf S) : Set L)
⊢ IsGLB S (sInf S)

Tactic:
apply IsGLB.of_image @h

Premises used: IsGLB.of_image
-- 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 (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), (↑K : Set L) ≤ (↑K' : Set L) ↔ K ≤ K'
simp : IsGLB (SetLike.coe '' S) (⋂ s ∈ S, (↑s : Set L))
⊢ IsGLB (SetLike.coe '' S) (↑(sInf S) : Set L)

Tactic:
simp only [coe_sInf]

Premises used: LieSubalgebra.coe_sInf
-- 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 (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), (↑K : Set L) ≤ (↑K' : Set L) ↔ K ≤ K'
⊢ IsGLB (SetLike.coe '' S) (⋂ s ∈ S, (↑s : Set L))

Tactic:
isGLB_biInf

Premises used: Set.iInter, isGLB_biInf
-- 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 (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), (↑K : Set L) ≤ (↑K' : Set L) ↔ K ≤ K'
⊢ IsGLB (SetLike.coe '' S) (⋂ s ∈ S, (↑s : Set L))

Tactic:
exact isGLB_biInf

Premises used: isGLB_biInf
-- 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 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
N : LieSubalgebra R L
x : L
h : Membership.mem (γ := LieSubalgebra R L) ⊥ x
⊢ x = 0

Tactic:
rw [mem_bot] at h

Premises used: LieSubalgebra.mem_bot
-- 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 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
N : LieSubalgebra R L
x : L
h : x = 0
rw : 0 ∈ N
⊢ x ∈ N

Tactic:
rw [h]
-- 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 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
N : LieSubalgebra R L
x : L
h : x = 0
⊢ 0 ∈ N

Tactic:
N.zero_mem'

Premises used: Submodule.toAddSubmonoid, Set.Mem, AddSubmonoid.zero_mem', LieSubalgebra.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
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
N : LieSubalgebra R L
x : L
h : x = 0
⊢ 0 ∈ N

Tactic:
exact N.zero_mem'

Premises used: Submodule.toAddSubmonoid, AddSubmonoid.zero_mem', LieSubalgebra.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
K K' : LieSubalgebra R L
⊢ K + K' = K ⊔ K'

Tactic:
rfl

Premises used: 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
⊢ (K ⊓ K').toSubmodule = K.toSubmodule ⊓ K'.toSubmodule

Tactic:
rfl

Premises used: 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
x : L
rw : x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K ∧ x ∈ K'
rw₁ : x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'
rw₂ : x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'.toSubmodule
rw₃ : x ∈ K.toSubmodule ⊓ K'.toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'.toSubmodule
rw₄ rw₅ : x ∈ K.toSubmodule ∧ x ∈ K'.toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'.toSubmodule
⊢ x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'

Tactic:
rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule,
    Submodule.mem_inf]

Premises used: LieSubalgebra.mem_toSubmodule, Submodule.mem_inf, LieSubalgebra.inf_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
K : LieSubalgebra R L
rw : K ≤ ⊥ ↔ ∀ x ∈ K, x = 0
⊢ K = ⊥ ↔ ∀ x ∈ K, x = 0

Tactic:
rw [_root_.eq_bot_iff]

Premises used: eq_bot_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
K : LieSubalgebra R L
⊢ K ≤ ⊥ ↔ ∀ x ∈ K, x = 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton
-- 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
⊢ K ≤ ⊥ ↔ ∀ x ∈ K, x = 0

Tactic:
exact Iff.rfl

Premises used: Iff.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 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
hα : Eq.{v + 1} (α := LieSubalgebra R ↥⊥) ⊥ ⊤
⊢ Subsingleton.{v + 1} (LieSubalgebra R ↥⊥)

Tactic:
apply subsingleton_of_bot_eq_top

Premises used: subsingleton_of_bot_eq_top
-- 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 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
hα :
  ∀ (x : L) (hx : Membership.mem (γ := LieSubalgebra R L) ⊥ x),
    Membership.mem (γ := LieSubalgebra R ↥⊥) ⊥
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) x hx) ↔
      Membership.mem (γ := LieSubalgebra R ↥⊥) ⊤
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) x hx)
⊢ Eq.{v + 1} (α := LieSubalgebra R ↥⊥) ⊥ ⊤

Tactic:
ext ⟨x, hx⟩
-- 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 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
hx : Membership.mem (γ := LieSubalgebra R L) ⊥ x
⊢ Membership.mem (γ := LieSubalgebra R L) ⊥ x

Tactic:
change x ∈ ⊥ at hx
-- 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 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
hx : Membership.mem (γ := LieSubalgebra R L) ⊥ x
⊢ x = 0

Tactic:
rw [LieSubalgebra.mem_bot] at hx

Premises used: LieSubalgebra.mem_bot
-- 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 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
hx_1 : Membership.mem (γ := LieSubalgebra R L) ⊥ x
hx : x = 0
hα :
  ∀ (hx : Membership.mem (γ := LieSubalgebra R L) ⊥ 0),
    Membership.mem (γ := LieSubalgebra R ↥⊥) ⊥
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) 0 hx) ↔
      Membership.mem (γ := LieSubalgebra R ↥⊥) ⊤
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) 0 hx)
⊢ Membership.mem (γ := LieSubalgebra R ↥⊥) ⊥
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) x hx_1) ↔
    Membership.mem (γ := LieSubalgebra R ↥⊥) ⊤
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) x hx_1)

Tactic:
subst hx
-- 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 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
hx : Membership.mem (γ := LieSubalgebra R L) ⊥ 0
hα : Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) 0 hx = 0
⊢ Membership.mem (γ := LieSubalgebra R ↥⊥) ⊥
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) 0 hx) ↔
    Membership.mem (γ := LieSubalgebra R ↥⊥) ⊤
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) 0 hx)

Tactic:
simp only [mem_bot, mem_top, iff_true]

Premises used: LieSubalgebra.mem_bot, iff_true, LieSubalgebra.mem_top
-- 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 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
hx : Membership.mem (γ := LieSubalgebra R L) ⊥ 0
⊢ Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) 0 hx = 0

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
⊢ Subsingleton.{v + 1} (↑(↑⊥ : Set L) : Type v)

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
K K' : LieSubalgebra R L
⊢ Disjoint K.toSubmodule K'.toSubmodule ↔ Disjoint K K'

Tactic:
simp [disjoint_iff, ← toSubmodule_inj]

Premises used: disjoint_iff, LieSubalgebra.toSubmodule_inj
-- 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 K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
inst_5 : IsNoetherian R L
⊢ WellFoundedGT.{v} (LieSubalgebra R L)

Tactic:
RelHomClass.isWellFounded (⟨toSubmodule, @fun _ _ h ↦ h⟩ : _ →r (· > ·))

Premises used: RelHom.mk, RelHomClass.isWellFounded, LieSubalgebra.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
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K
⊢ (↑((inclusion h : (a : ↥K) → ↥K') x) : L) = (↑x : L)

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
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K
⊢ (inclusion h : (a : ↥K) → ↥K') x = Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑x : L) ⋯

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
K K' : LieSubalgebra R L
h : K ≤ K'
x y : ↥K
⊢ Eq (α := ↥K') ((inclusion h : (a : ↥K) → ↥K') x : ↥K') ((inclusion h : (a : ↥K) → ↥K') y : ↥K') → x = y

Tactic:
simp only [inclusion_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]

Premises used: LieSubalgebra.inclusion_apply, SetLike.coe_eq_coe, imp_self, Subtype.mk_eq_mk
-- 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'
simp : (∃ (y : ↥K), Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑y : L) ⋯ = x) ↔ (↑x : L) ∈ K
⊢ x ∈ ofLe h ↔ (↑x : L) ∈ K

Tactic:
simp only [ofLe, inclusion_apply, LieHom.mem_range]

Premises used: LieSubalgebra.inclusion_apply, LieSubalgebra.ofLe, LieHom.mem_range
-- 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'
mp : (∃ (y : ↥K), Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑y : L) ⋯ = x) → (↑x : L) ∈ K
mpr : (↑x : L) ∈ K → ∃ (y : ↥K), Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑y : L) ⋯ = x
⊢ (∃ (y : ↥K), Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑y : L) ⋯ = x) ↔ (↑x : L) ∈ K

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
K K' : LieSubalgebra R L
h : K ≤ K'
y : ↥K
⊢ (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑y : L) ⋯) : L) ∈ K

Tactic:
y.property

Premises used: Set.Mem, Subtype.property
-- 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'
y : ↥K
⊢ (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑y : L) ⋯) : L) ∈ K

Tactic:
exact y.property

Premises used: Subtype.property
-- 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_1 : K ≤ K'
x : ↥K'
h : (↑x : L) ∈ K
w : ↥K
h₁ : Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ K) (↑x : L) h) : L) ⋯ = x
⊢ ∃ (y : ↥K), Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑y : L) ⋯ = x

Tactic:
use ⟨(x : L), h⟩
-- 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'
h₁ : ∀ (x : ↥K'), x ∈ ofLe h ↔ x ∈ comap K'.incl K
⊢ ofLe h = comap K'.incl K

Tactic:
ext