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' : LieSubalgebra R L
x y : L
hx : x ∈ L'
hy : y ∈ L'
⊢ ⁅x, y⁆ ∈ L'

Tactic:
L'.lie_mem' hx hy

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' : LieSubalgebra R L
x : L
⊢ x ∈ L'.carrier ↔ x ∈ (↑L' : Set L)

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
S : Set L
h₁ : ∀ {a b : L}, a ∈ S → b ∈ S → a + b ∈ S
h₂ : S 0
h₃ :
  ∀ (c : R) {x : L},
    x ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂ : AddSubmonoid L }.carrier →
      c • x ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂ : AddSubmonoid L }.carrier
h₄ :
  ∀ {x y : L},
    x ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂, smul_mem' := h₃ : Submodule R L }.carrier →
      y ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂, smul_mem' := h₃ : Submodule R L }.carrier →
        ⁅x, y⁆ ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂, smul_mem' := h₃ : Submodule R L }.carrier
x : L
⊢ x ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem' := @h₄ : LieSubalgebra R L } ↔ x ∈ S

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

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
p : Submodule R L
h : ∀ {x y : L}, x ∈ p.carrier → y ∈ p.carrier → ⁅x, y⁆ ∈ p.carrier
x : L
⊢ x ∈ { toSubmodule := p, lie_mem' := @h : LieSubalgebra R L } ↔ x ∈ p

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

Tactic:
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' : LieSubalgebra R L
x y : ↥L'
⊢ (↑⁅x, y⁆ : L) = ⁅(↑x : L), (↑y : L)⁆

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
L' : LieSubalgebra R L
x y : ↥L'
⊢ x = y ↔ (↑x : L) = (↑y : L)

Tactic:
Subtype.ext_iff

Premises used: Subtype.ext_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' : LieSubalgebra R L
x : ↥L'
⊢ (↑x : L) = 0 ↔ x = 0

Tactic:
(ext_iff L' x 0).symm

Premises used: LieSubalgebra.ext_iff, OfNat.ofNat, Iff.symm
-- 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₁' L₂' : LieSubalgebra R L
h : ∀ (x : L), x ∈ L₁' ↔ x ∈ L₂'
⊢ L₁' = L₂'

Tactic:
SetLike.ext h

Premises used: SetLike.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₁' L₂' : LieSubalgebra R L
⊢ L₁' = L₂' ↔ ∀ (x : L), x ∈ L₁' ↔ x ∈ L₂'

Tactic:
SetLike.ext_iff

Premises used: SetLike.ext_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
h₁ : ∀ {a b : L}, a ∈ S → b ∈ S → a + b ∈ S
h₂ : S 0
h₃ :
  ∀ (c : R) {x : L},
    x ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂ : AddSubmonoid L }.carrier →
      c • x ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂ : AddSubmonoid L }.carrier
h₄ :
  ∀ {x y : L},
    x ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂, smul_mem' := h₃ : Submodule R L }.carrier →
      y ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂, smul_mem' := h₃ : Submodule R L }.carrier →
        ⁅x, y⁆ ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂, smul_mem' := h₃ : Submodule R L }.carrier
⊢ (↑{ carrier := S, add_mem' := @h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem' := @h₄ : LieSubalgebra R L } : Set L) =
    S

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
p : Submodule R L
h : ∀ {x y : L}, x ∈ p.carrier → y ∈ p.carrier → ⁅x, y⁆ ∈ p.carrier
⊢ { toSubmodule := p, lie_mem' := @h : LieSubalgebra R L }.toSubmodule = p

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
⊢ Function.Injective (α := LieSubalgebra R L) SetLike.coe

Tactic:
SetLike.coe_injective

Premises used: SetLike.coe_injective
-- 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₁' L₂' : LieSubalgebra R L
⊢ (↑L₁' : Set L) = (↑L₂' : Set L) ↔ L₁' = L₂'

Tactic:
SetLike.coe_set_eq

Premises used: SetLike.coe_set_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
L₁' L₂' : LieSubalgebra R L
h : L₁'.toSubmodule = L₂'.toSubmodule
⊢ (↑L₁'.toSubmodule : Set L) = (↑L₂'.toSubmodule : Set L)

Tactic:
rw [SetLike.ext'_iff] at h

Premises used: SetLike.ext'_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₁' L₂' : LieSubalgebra R L
h : (↑L₁'.toSubmodule : Set L) = (↑L₂'.toSubmodule : Set L)
rw : (↑L₁' : Set L) = (↑L₂' : Set L)
⊢ L₁' = L₂'

Tactic:
rw [← coe_set_eq]

Premises used: LieSubalgebra.coe_set_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
L₁' L₂' : LieSubalgebra R L
h : (↑L₁'.toSubmodule : Set L) = (↑L₂'.toSubmodule : Set L)
⊢ (↑L₁' : Set L) = (↑L₂' : Set L)

Tactic:
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₁' L₂' : LieSubalgebra R L
h : (↑L₁'.toSubmodule : Set L) = (↑L₂'.toSubmodule : Set L)
⊢ (↑L₁' : Set L) = (↑L₂' : Set L)

Tactic:
exact 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₁' L₂' : LieSubalgebra R L
⊢ L₁'.toSubmodule = L₂'.toSubmodule ↔ L₁' = L₂'

Tactic:
toSubmodule_injective.eq_iff

Premises used: Function.Injective.eq_iff, LieSubalgebra.toSubmodule_injective
-- 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' : LieSubalgebra R L
⊢ (↑L'.toSubmodule : Set L) = (↑L' : Set L)

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
L' : LieSubalgebra R L
M : Type w
inst_3 : AddCommGroup M
inst_4 : LieRingModule L M
x : ↥L'
m : M
⊢ ⁅x, m⁆ = ⁅(↑x : L), m⁆

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
L' : LieSubalgebra R L
M : Type w
inst_3 : AddCommGroup M
inst_4 : LieRingModule L M
N : Type w₁
inst_5 : AddCommGroup N
inst_6 : LieRingModule L N
inst_7 : Module R N
inst_8 : Module R M
inst_9 : LieModule R L M
t : R
x : ↥L'
m : M
rw : ⁅(↑(t • x) : L), m⁆ = t • ⁅x, m⁆
rw₁ : ⁅t • (↑x : L), m⁆ = t • ⁅x, m⁆
rw₂ : t • ⁅(↑x : L), m⁆ = t • ⁅x, m⁆
rw₃ rw₄ : t • ⁅(↑x : L), m⁆ = t • ⁅(↑x : L), m⁆
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
rw [coe_bracket_of_module, Submodule.coe_smul_of_tower, smul_lie, coe_bracket_of_module]

Premises used: LieSubalgebra.coe_bracket_of_module, smul_lie, Submodule.coe_smul_of_tower
-- 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' : LieSubalgebra R L
M : Type w
inst_3 : AddCommGroup M
inst_4 : LieRingModule L M
N : Type w₁
inst_5 : AddCommGroup N
inst_6 : LieRingModule L N
inst_7 : Module R N
inst_8 : Module R M
inst_9 : LieModule R L M
t : R
x : ↥L'
m : M
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
simp only [coe_bracket_of_module, lie_smul]

Premises used: lie_smul, LieSubalgebra.coe_bracket_of_module
-- 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' : LieSubalgebra R L
M : Type w
inst_3 : AddCommGroup M
inst_4 : LieRingModule L M
N : Type w₁
inst_5 : AddCommGroup N
inst_6 : LieRingModule L N
inst_7 : Module R N
inst_8 : Module R M
f : M →ₗ⁅R,L⁆ N
⊢ Eq (α := (a : M) → N) (⇑(f.restrictLie L') : (a : M) → N) (⇑f : (a : M) → N)

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
L' : LieSubalgebra R L
⊢ Eq (α := (a : ↥L') → L) (⇑L'.incl : (a : ↥L') → L) (Subtype.val (p := fun (x : L) ↦ x ∈ L'))

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
L' : LieSubalgebra R L
⊢ Eq (α := (a : ↥L') → L) (⇑L'.incl' : (a : ↥L') → L) (Subtype.val (p := fun (x : L) ↦ x ∈ L'))

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

Tactic:
⟨⁅x, y⁆, f.map_lie x y⟩

Premises used: Set.Mem, Bracket.bracket, setOf, LieHom.map_lie, Exists.intro, Set.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
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x y : L
⊢ Membership.mem (α := L₂) (↑f : L →ₗ[R] L₂).range.carrier
    (Bracket.bracket (L := L₂) (((↑f : L →ₗ[R] L₂) : (a : L) → L₂) x : L₂) (((↑f : L →ₗ[R] L₂) : (a : L) → L₂) y) : L₂)

Tactic:
exact ⟨⁅x, y⁆, f.map_lie x y⟩
-- 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₂
⊢ (↑f.range : Set L₂) = Set.range.{w, v + 1} (ι := L) (⇑f : (a : L) → L₂)

Tactic:
LinearMap.coe_range (f : L →ₗ[R] L₂)

Premises used: LinearMap.coe_range, LieHom.toLinearMap
-- 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 ↔ ∃ (y : L), (f : (a : L) → L₂) y = x

Tactic:
LinearMap.mem_range

Premises used: Set.Mem, LinearMap.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
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
⊢ Membership.mem (α := L₂) f.range ((f : (a : L) → L₂) x : L₂)

Tactic:
LinearMap.mem_range_self (f : L →ₗ[R] L₂) x

Premises used: Set.Mem, LinearMap.mem_range_self, LieHom.toLinearMap
-- 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 y : L
a :
  (↑(AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) ⁅x, y⁆) : L₂) =
    (↑(Bracket.bracket (L := ↥f.range)
          (AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) x : ↥(↑f : L →ₗ[R] L₂).range)
          (AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) y)) :
      L₂)
⊢ Eq (α := ↥f.range)
    (AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) ⁅x, y⁆ : ↥(↑f : L →ₗ[R] L₂).range)
    (Bracket.bracket (L := ↥f.range)
      (AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) x : ↥(↑f : L →ₗ[R] L₂).range)
      (AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) y))

Tactic:
apply Subtype.ext

Premises used: Subtype.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 y : L
⊢ (↑(AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) ⁅x, y⁆) : L₂) =
    (↑(Bracket.bracket (L := ↥f.range)
          (AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) x : ↥(↑f : L →ₗ[R] L₂).range)
          (AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) y)) :
      L₂)

Tactic:
f.map_lie x y

Premises used: LieHom.map_lie
-- 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 y : L
⊢ (↑(AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) ⁅x, y⁆) : L₂) =
    (↑(Bracket.bracket (L := ↥f.range)
          (AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) x : ↥(↑f : L →ₗ[R] L₂).range)
          (AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) y)) :
      L₂)

Tactic:
exact f.map_lie x y

Premises used: LieHom.map_lie
-- 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
⊢ Eq.{w + 1} (α := ↥f.range) ((f.rangeRestrict : (a : L) → ↥f.range) x : ↥f.range)
    (Subtype.mk (p := fun (x : L₂) ↦ x ∈ f.range) ((f : (a : L) → L₂) x) ⋯ : ↥f.range)

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₂
y : L₂
hy : y ∈ f.range
⊢ ∃ (y_1 : L), (f : (a : L) → L₂) y_1 = y

Tactic:
rw [mem_range] at hy

Premises used: 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
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy_1 : y ∈ f.range
hy : ∃ (y_1 : L), (f : (a : L) → L₂) y_1 = y
obtain :
  ∀ (x : L) (hy : Membership.mem (α := L₂) f.range ((f : (a : L) → L₂) x : L₂)),
    ∃ (a : L),
      Eq.{w + 1} (α := ↥f.range) ((f.rangeRestrict : (a : L) → ↥f.range) a : ↥f.range)
        (Subtype.mk (p := fun (x : L₂) ↦ x ∈ f.range) ((f : (a : L) → L₂) x) hy : ↥f.range)
⊢ ∃ (a : L), (f.rangeRestrict : (a : L) → ↥f.range) a = Subtype.mk (p := fun (x : L₂) ↦ x ∈ f.range) y hy_1

Tactic:
obtain ⟨x, rfl⟩ := hy

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
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : Membership.mem (α := L₂) f.range ((f : (a : L) → L₂) x : L₂)
h :
  Eq.{w + 1} (α := ↥f.range) ((f.rangeRestrict : (a : L) → ↥f.range) x : ↥f.range)
    (Subtype.mk (p := fun (x : L₂) ↦ x ∈ f.range) ((f : (a : L) → L₂) x) hy : ↥f.range)
⊢ ∃ (a : L),
    Eq.{w + 1} (α := ↥f.range) ((f.rangeRestrict : (a : L) → ↥f.range) a : ↥f.range)
      (Subtype.mk (p := fun (x : L₂) ↦ x ∈ f.range) ((f : (a : L) → L₂) x) hy : ↥f.range)

Tactic:
use 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
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : Membership.mem (α := L₂) f.range ((f : (a : L) → L₂) x : L₂)
⊢ Eq.{w + 1} (α := ↥f.range) ((f.rangeRestrict : (a : L) → ↥f.range) x : ↥f.range)
    (Subtype.mk (p := fun (x : L₂) ↦ x ∈ f.range) ((f : (a : L) → L₂) x) hy : ↥f.range)

Tactic:
simp only [rangeRestrict_apply]

Premises used: LieHom.rangeRestrict_apply
-- 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 : Function.Injective.{v + 1, w + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
x y : L
hxy :
  Eq.{w + 1} (α := ↥f.range) ((f.rangeRestrict : (a : L) → ↥f.range) x : ↥f.range)
    ((f.rangeRestrict : (a : L) → ↥f.range) y : ↥f.range)
⊢ Eq.{w + 1} (α := L₂) ((f : (a : L) → L₂) x : L₂) ((f : (a : L) → L₂) y : L₂)

Tactic:
simp only [Subtype.mk_eq_mk, rangeRestrict_apply] at hxy

Premises used: LieHom.rangeRestrict_apply, 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
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
h : Function.Injective.{v + 1, w + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
x y : L
hxy : Eq.{w + 1} (α := L₂) ((f : (a : L) → L₂) x : L₂) ((f : (a : L) → L₂) y : L₂)
⊢ x = y

Tactic:
h hxy
-- 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 : Function.Injective.{v + 1, w + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
x y : L
hxy : Eq.{w + 1} (α := L₂) ((f : (a : L) → L₂) x : L₂) ((f : (a : L) → L₂) y : L₂)
⊢ x = y

Tactic:
exact h hxy
-- 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 : Function.Injective.{v + 1, w + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
x : L
⊢ Eq.{w + 1} (α := ↥f.range) ((f.equivRangeOfInjective h : (a : L) → ↥f.range) x : ↥f.range)
    (Subtype.mk (p := fun (x : L₂) ↦ x ∈ f.range) ((f : (a : L) → L₂) x) ⋯ : ↥f.range)

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
p : Submodule R L
mp : (∃ (K : LieSubalgebra R L), K.toSubmodule = p) → ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
mpr : (∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p) → ∃ (K : LieSubalgebra R L), K.toSubmodule = p
⊢ (∃ (K : LieSubalgebra R L), K.toSubmodule = 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
K : LieSubalgebra R L
x y : L
⊢ x ∈ K.toSubmodule → y ∈ K.toSubmodule → ⁅x, y⁆ ∈ K.toSubmodule

Tactic:
K.lie_mem'

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
K : LieSubalgebra R L
x y : L
⊢ x ∈ K.toSubmodule → y ∈ K.toSubmodule → ⁅x, y⁆ ∈ K.toSubmodule

Tactic:
exact K.lie_mem'

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
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
w : LieSubalgebra R L
h₁ : { toSubmodule := p, lie_mem' := ⋯ : LieSubalgebra R L }.toSubmodule = p
⊢ ∃ (K : LieSubalgebra R L), K.toSubmodule = p

Tactic:
use { p with lie_mem' := 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 : LieSubalgebra R L
rw : K.incl.range.toSubmodule = K.toSubmodule
⊢ K.incl.range = K

Tactic:
rw [← 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
K : LieSubalgebra R L
⊢ K.incl.range.toSubmodule = K.toSubmodule

Tactic:
(K : Submodule R L).range_subtype

Premises used: Set.Mem, LinearMap.range, Submodule.range_subtype, LieSubalgebra.toSubmodule, 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 : LieSubalgebra R L
⊢ K.incl.range.toSubmodule = K.toSubmodule

Tactic:
exact (K : Submodule R L).range_subtype

Premises used: Submodule.range_subtype, 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₂
x y : L₂
hx : x ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
hy : y ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
⊢ x ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).toAddSubsemigroup

Tactic:
simp only [AddSubsemigroup.mem_carrier] at hx hy

Premises used: AddSubsemigroup.mem_carrier
-- 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.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
hy : y ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
hx₁ : x ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).toAddSubsemigroup
⊢ y ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).toAddSubsemigroup

Tactic:
simp only [AddSubsemigroup.mem_carrier] at hx hy

Premises used: AddSubsemigroup.mem_carrier
-- 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.map (↑f : L →ₗ[R] L₂) K.toSubmodule).toAddSubsemigroup
hy : y ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).toAddSubsemigroup
rcases :
  ∀ (x' : L) (hx' : x' ∈ (↑K.toSubmodule : Set L)),
    Bracket.bracket (L := L₂) (((↑f : L →ₗ[R] L₂) : (a : L) → L₂) x' : L₂) y ∈
      (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
⊢ ⁅x, y⁆ ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier

Tactic:
rcases hx with ⟨x', hx', 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
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₂
y : L₂
hy : y ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).toAddSubsemigroup
x' : L
hx' : x' ∈ (↑K.toSubmodule : Set L)
rcases :
  ∀ (y' : L) (hy' : y' ∈ (↑K.toSubmodule : Set L)),
    Membership.mem (α := L₂) (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
      (Bracket.bracket (L := L₂) (((↑f : L →ₗ[R] L₂) : (a : L) → L₂) x' : L₂) (((↑f : L →ₗ[R] L₂) : (a : L) → L₂) y') :
        L₂)
⊢ Bracket.bracket (L := L₂) (((↑f : L →ₗ[R] L₂) : (a : L) → L₂) x' : L₂) y ∈
    (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier

Tactic:
rcases hy with ⟨y', hy', 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
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' : x' ∈ (↑K.toSubmodule : Set L)
y' : L
hy' : y' ∈ (↑K.toSubmodule : Set L)
⊢ Membership.mem (α := L₂) (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
    (Bracket.bracket (L := L₂) (((↑f : L →ₗ[R] L₂) : (a : L) → L₂) x' : L₂) (((↑f : L →ₗ[R] L₂) : (a : L) → L₂) y') :
      L₂)

Tactic:
simpa using ⟨⁅x', y'⁆, K.lie_mem hx' hy', f.map_lie x' y'⟩
-- 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 ∈ map f K ↔ ∃ y ∈ K, (f : (a : L) → L₂) y = x

Tactic:
Submodule.mem_map

Premises used: Set.Mem, Submodule.mem_map