awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
x y : ↥L₁'
⊢ (↑((↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯) : ↥L₁'.toSubmodule →ₗ[R] ↥L₂'.toSubmodule).toFun
          ⁅x, y⁆) :
      L₂) =
    (↑⁅(↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯) :
                ↥L₁'.toSubmodule →ₗ[R] ↥L₂'.toSubmodule).toFun
            x,
          (↑(e.toLinearEquiv.ofSubmodules L₁'.toSubmodule L₂'.toSubmodule ⋯) :
                ↥L₁'.toSubmodule →ₗ[R] ↥L₂'.toSubmodule).toFun
            y⁆ :
      L₂)

Tactic:
exact LieHom.map_lie (↑e : L₁ →ₗ⁅R⁆ L₂) ↑x ↑y

Premises used: LieEquiv.toLieHom, LieHom.map_lie, Subtype.val
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
L₁' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
x : ↥L₁'
⊢ Eq.{w + 1} (α := L₂) ((↑((ofSubalgebras L₁' L₂' e h : (a : ↥L₁') → ↥L₂') x) : L₂) : L₂)
    ((e : (a : L₁) → L₂) (↑x : L₁) : L₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Subalgebra
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
L₁' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
x : ↥L₂'
⊢ Eq.{v + 1} (α := L₁) ((↑(((ofSubalgebras L₁' L₂' e h).symm : (a : ↥L₂') → ↥L₁') x) : L₁) : L₁)
    ((e.symm : (a : L₂) → L₁) (↑x : L₂) : L₁)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N_1 N' N O : LieSubmodule R L M
h :
  Eq.{w + 1} (α := Set M) ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier) N)
    ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier) O)
mk :
  ∀ (toSubmodule : Submodule R M) (lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier)
    (h :
      Eq.{w + 1} (α := Set M)
        ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier)
          { toSubmodule := toSubmodule, lie_mem := @lie_mem })
        ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier) O)),
    { toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } = O
⊢ N = O

Tactic:
cases N
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' O : LieSubmodule R L M
toSubmodule : Submodule R M
lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier
h :
  Eq.{w + 1} (α := Set M)
    ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier) { toSubmodule := toSubmodule, lie_mem := @lie_mem })
    ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier) O)
mk :
  ∀ (toSubmodule_1 : Submodule R M)
    (lie_mem_1 : ∀ {x : L} {m : M}, m ∈ toSubmodule_1.carrier → ⁅x, m⁆ ∈ toSubmodule_1.carrier)
    (h :
      Eq.{w + 1} (α := Set M)
        ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier)
          { toSubmodule := toSubmodule, lie_mem := @lie_mem })
        ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier)
          { toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 })),
    { toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } =
      { toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 }
⊢ { toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } = O

Tactic:
cases O
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
toSubmodule : Submodule R M
lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier
toSubmodule_1 : Submodule R M
lie_mem_1 : ∀ {x : L} {m : M}, m ∈ toSubmodule_1.carrier → ⁅x, m⁆ ∈ toSubmodule_1.carrier
h :
  Eq.{w + 1} (α := Set M)
    ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier) { toSubmodule := toSubmodule, lie_mem := @lie_mem })
    ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier)
      { toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 })
mk : toSubmodule = toSubmodule_1
⊢ { toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } =
    { toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
toSubmodule : Submodule R M
lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier
toSubmodule_1 : Submodule R M
lie_mem_1 : ∀ {x : L} {m : M}, m ∈ toSubmodule_1.carrier → ⁅x, m⁆ ∈ toSubmodule_1.carrier
h :
  Eq.{w + 1} (α := Set M)
    ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier) { toSubmodule := toSubmodule, lie_mem := @lie_mem })
    ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier)
      { toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 })
⊢ toSubmodule = toSubmodule_1

Tactic:
SetLike.coe_injective' h

Premises used: SetLike.coe_injective'
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
toSubmodule : Submodule R M
lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier
toSubmodule_1 : Submodule R M
lie_mem_1 : ∀ {x : L} {m : M}, m ∈ toSubmodule_1.carrier → ⁅x, m⁆ ∈ toSubmodule_1.carrier
h :
  Eq.{w + 1} (α := Set M)
    ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier) { toSubmodule := toSubmodule, lie_mem := @lie_mem })
    ((fun (s : LieSubmodule R L M) ↦ (↑s : Submodule R M).carrier)
      { toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 })
⊢ toSubmodule = toSubmodule_1

Tactic:
exact SetLike.coe_injective' h

Premises used: SetLike.coe_injective'
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
x : L
m : M
h :
  Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, w} (R := R) 0))) m
rw :
  Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, w} (R := R) 0))) ⁅x, 0⁆
⊢ Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, w} (R := R) 0))) ⁅x, m⁆

Tactic:
rw [(Submodule.mem_bot R).1 h]

Premises used: Submodule.mem_bot, Iff.mp
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
x : L
m : M
h :
  Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, w} (R := R) 0))) m
⊢ Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, w} (R := R) 0))) ⁅x, 0⁆

Tactic:
apply lie_zero

Premises used: lie_zero
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
⊢ (↑(↑N : Submodule R M) : Set M) = (↑N : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
x : M
⊢ x ∈ (↑N : Submodule R M).carrier ↔ x ∈ (↑N : Set M)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
S : Set M
h₁ : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S
h₂ : S 0
h₃ :
  ∀ (c : R) {x : M},
    x ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂ : AddSubmonoid M }.carrier →
      c • x ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂ : AddSubmonoid M }.carrier
h₄ :
  ∀ {x : L} {m : M},
    m ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂, smul_mem' := h₃ : Submodule R M }.carrier →
      ⁅x, m⁆ ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂, smul_mem' := h₃ : Submodule R M }.carrier
x : M
⊢ x ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem := @h₄ : LieSubmodule R L M } ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
p : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier
x : M
⊢ x ∈ { toSubmodule := p, lie_mem := @h : LieSubmodule R L M } ↔ x ∈ p

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
x : M
⊢ x ∈ (↑N : Submodule R M) ↔ x ∈ N

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
x : M
⊢ x ∈ (↑N : Set M) ↔ x ∈ N

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
⊢ 0 ∈ N

Tactic:
zero_mem N

Premises used: Set.Mem, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
x : M
h : x ∈ N
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ N) x h = 0 ↔ x = 0

Tactic:
Subtype.ext_iff

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
S : Set M
h₁ : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S
h₂ : S 0
h₃ :
  ∀ (c : R) {x : M},
    x ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂ : AddSubmonoid M }.carrier →
      c • x ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂ : AddSubmonoid M }.carrier
h₄ :
  ∀ {x : L} {m : M},
    m ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂, smul_mem' := h₃ : Submodule R M }.carrier →
      ⁅x, m⁆ ∈ { carrier := S, add_mem' := @h₁, zero_mem' := h₂, smul_mem' := h₃ : Submodule R M }.carrier
⊢ (↑{ carrier := S, add_mem' := @h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem := @h₄ : LieSubmodule R L M } : Set M) =
    S

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
p : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier
mk :
  ∀ (toAddSubmonoid : AddSubmonoid M)
    (smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier)
    (h :
      ∀ {x : L} {m : M},
        m ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R M }.carrier →
          ⁅x, m⁆ ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R M }.carrier),
    (↑{ toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem := @h : LieSubmodule R L M } :
        Submodule R M) =
      { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' }
⊢ (↑{ toSubmodule := p, lie_mem := @h : LieSubmodule R L M } : Submodule R M) = p

Tactic:
cases p
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
toAddSubmonoid : AddSubmonoid M
smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier
h :
  ∀ {x : L} {m : M},
    m ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R M }.carrier →
      ⁅x, m⁆ ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R M }.carrier
⊢ (↑{ toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem := @h : LieSubmodule R L M } : Submodule R M) =
    { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' }

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
x y : LieSubmodule R L M
h : (↑x : Submodule R M) = (↑y : Submodule R M)
mk :
  ∀ (toSubmodule : Submodule R M) (lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier)
    (h :
      (↑{ toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } : Submodule R M) =
        (↑y : Submodule R M)),
    { toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } = y
⊢ x = y

Tactic:
cases x
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
y : LieSubmodule R L M
toSubmodule : Submodule R M
lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier
h : (↑{ toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } : Submodule R M) = (↑y : Submodule R M)
mk :
  ∀ (toSubmodule_1 : Submodule R M)
    (lie_mem_1 : ∀ {x : L} {m : M}, m ∈ toSubmodule_1.carrier → ⁅x, m⁆ ∈ toSubmodule_1.carrier)
    (h :
      (↑{ toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } : Submodule R M) =
        (↑{ toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 : LieSubmodule R L M } : Submodule R M)),
    { toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } =
      { toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 }
⊢ { toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } = y

Tactic:
cases y
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
toSubmodule : Submodule R M
lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier
toSubmodule_1 : Submodule R M
lie_mem_1 : ∀ {x : L} {m : M}, m ∈ toSubmodule_1.carrier → ⁅x, m⁆ ∈ toSubmodule_1.carrier
h :
  (↑{ toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } : Submodule R M) =
    (↑{ toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 : LieSubmodule R L M } : Submodule R M)
⊢ { toSubmodule := toSubmodule, lie_mem := @lie_mem : LieSubmodule R L M } =
    { toSubmodule := toSubmodule_1, lie_mem := @lie_mem_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
h : ∀ (m : M), m ∈ N ↔ m ∈ N'
⊢ N = N'

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
⊢ (↑N : Submodule R M) = (↑N' : Submodule R M) ↔ N = N'

Tactic:
toSubmodule_injective.eq_iff

Premises used: LieSubmodule.toSubmodule_injective, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
s : Set M
hs : s = (↑N : Set M)
a b : M
x : a ∈ s
y : b ∈ s
rw : ∀ (x : a ∈ (↑N : Set M)) (y : b ∈ (↑N : Set M)), a + b ∈ (↑N : Set M)
⊢ a + b ∈ s

Tactic:
rw [hs] at x y ⊢
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
s : Set M
hs : s = (↑N : Set M)
a b : M
x : a ∈ (↑N : Set M)
y : b ∈ (↑N : Set M)
⊢ a + b ∈ (↑N : Set M)

Tactic:
N.add_mem' x y

Premises used: Submodule.toAddSubmonoid, Set.Mem, LieSubmodule.toSubmodule, AddSubmonoid.toAddSubsemigroup, AddSubsemigroup.add_mem'
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
s : Set M
hs : s = (↑N : Set M)
a b : M
x : a ∈ (↑N : Set M)
y : b ∈ (↑N : Set M)
⊢ a + b ∈ (↑N : Set M)

Tactic:
exact N.add_mem' x y

Premises used: Submodule.toAddSubmonoid, LieSubmodule.toSubmodule, AddSubmonoid.toAddSubsemigroup, AddSubsemigroup.add_mem'
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
s : Set M
hs : s = (↑N : Set M)
⊢ 0 ∈ s

Tactic:
simp [hs]
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
s : Set M
hs : s = (↑N : Set M)
⊢ ∀ (c : R) {x : M}, x ∈ s → c • x ∈ s

Tactic:
hs.symm ▸ N.smul_mem'

Premises used: Submodule.smul_mem', LieSubmodule.toSubmodule, Eq.rec, Eq.symm
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
s : Set M
hs : s = (↑N : Set M)
⊢ ∀ (c : R) {x : M}, x ∈ s → c • x ∈ s

Tactic:
exact hs.symm ▸ N.smul_mem'
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
s : Set M
hs : s = (↑N : Set M)
x : L
m : M
⊢ m ∈ s → ⁅x, m⁆ ∈ s

Tactic:
hs.symm ▸ N.lie_mem

Premises used: Eq.rec, LieSubmodule.lie_mem, Eq.symm
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
s : Set M
hs : s = (↑N : Set M)
⊢ ∀ {x : L} {m : M}, m ∈ s → ⁅x, m⁆ ∈ s

Tactic:
exact hs.symm ▸ N.lie_mem
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
S : LieSubmodule R L M
s : Set M
hs : s = (↑S : Set M)
⊢ (↑(S.copy s hs) : Set M) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
S : LieSubmodule R L M
s : Set M
hs : s = (↑S : Set M)
⊢ S.copy s hs = S

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
x y : L
m : ↥N
a :
  (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x + y, (↑m : M)⁆ ⋯) : M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑m : M)⁆ ⋯ + Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑m : M)⁆ ⋯) :
      M)
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x + y, (↑m : M)⁆ ⋯ =
    Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑m : M)⁆ ⋯ + Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑m : M)⁆ ⋯

Tactic:
apply SetCoe.ext

Premises used: SetCoe.ext
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
x y : L
m : ↥N
⊢ (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x + y, (↑m : M)⁆ ⋯) : M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑m : M)⁆ ⋯ + Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑m : M)⁆ ⋯) :
      M)

Tactic:
apply add_lie

Premises used: add_lie
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
x : L
m n : ↥N
a :
  (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑(m + n) : M)⁆ ⋯) : M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑m : M)⁆ ⋯ + Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑n : M)⁆ ⋯) :
      M)
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑(m + n) : M)⁆ ⋯ =
    Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑m : M)⁆ ⋯ + Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑n : M)⁆ ⋯

Tactic:
apply SetCoe.ext

Premises used: SetCoe.ext
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
x : L
m n : ↥N
⊢ (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑(m + n) : M)⁆ ⋯) : M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑m : M)⁆ ⋯ + Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑n : M)⁆ ⋯) :
      M)

Tactic:
apply lie_add

Premises used: lie_add
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
x y : L
m : ↥N
a :
  (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑m : M)⁆ ⋯) : M)⁆ ⋯) : M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅⁅x, y⁆, (↑m : M)⁆ ⋯ +
          Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑m : M)⁆ ⋯) : M)⁆ ⋯) :
      M)
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑m : M)⁆ ⋯) : M)⁆ ⋯ =
    Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅⁅x, y⁆, (↑m : M)⁆ ⋯ +
      Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑m : M)⁆ ⋯) : M)⁆ ⋯

Tactic:
apply SetCoe.ext

Premises used: SetCoe.ext
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
x y : L
m : ↥N
⊢ (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑m : M)⁆ ⋯) : M)⁆ ⋯) : M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅⁅x, y⁆, (↑m : M)⁆ ⋯ +
          Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅x, (↑m : M)⁆ ⋯) : M)⁆ ⋯) :
      M)

Tactic:
apply leibniz_lie

Premises used: leibniz_lie
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
⊢ Eq.{w + 1} (α := M) (↑0 : M) 0

Tactic:
rfl

Premises used: rfl