mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
x : R
⊢ I x ≤ Ideal.span {x}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : q < 0
⊢ coreE₂Cohomological.i₂ (p, q) ≤ WithBotTop.coe 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject C EInt
inst✝ : Y.IsFirstQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : p < 0
⊢ WithBotTop.coe (coreE₂Cohomological.deg (p, q)) < coreE₂Cohomological.i₁ (p, q)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : 0 < q
⊢ IsZero ((Y.E₂SpectralSequence.page r ⋯).X (p, q))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : 0 < p
⊢ IsZero ((Y.E₂SpectralSequence.page r ⋯).X (p, q))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ ⁅x✝² + x✝¹, x✝⁆ = ⁅x✝², x✝⁆ + ⁅x✝¹, x✝⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ ⁅x✝², x✝¹ + x✝⁆ = ⁅x✝², x✝¹⁆ + ⁅x✝², x✝⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝ : Ring A
⊢ ∀ (x : A), ⁅x, x⁆ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝ : Ring A
x✝² x✝¹ x✝ : A
⊢ ⁅x✝², ⁅x✝¹, x✝⁆⁆ = ⁅⁅x✝², x✝¹⁆, x✝⁆ + ⁅x✝¹, ⁅x✝², x✝⁆⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝² : Ring A
M : Type w
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ ∀ (x y : A) (m : M), x • y • m = ⁅x, y⁆ • m + y • x • m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝² : Ring A
R : Type u
inst✝¹ : CommRing R
inst✝ : Algebra R A
t : R
x y : A
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝⁶ : Ring A
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R A
B : Type w
C : Type w₁
inst✝³ : Ring B
inst✝² : Ring C
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
g : B →ₐ[R] C
x✝¹ x✝ : A
⊢ f.toLinearMap.toFun ⁅x✝¹, x✝⁆ = ⁅f.toLinearMap.toFun x✝¹, f.toLinearMap.toFun x✝⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: A : Type v
inst✝⁴ : Ring A
R : Type u
inst✝³ : CommRing R
inst✝² : Algebra R A
B : Type w
inst✝¹ : Ring B
inst✝ : Algebra R B
f g : A →ₐ[R] B
h : f.toLieHom = g.toLieHom
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
⊢ { toFun := fun m ↦ ⁅x + y, m⁆, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun m ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun m ↦ ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
t : R
x : L
⊢ { toFun := fun m ↦ ⁅t • x, m⁆, map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) t • { toFun := fun m ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
⊢ { toFun := fun m ↦ ⁅⁅x, y⁆, m⁆, map_add' := ⋯, map_smul' := ⋯ } =
    ⁅{ toFun := fun m ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ },
      { toFun := fun m ↦ ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ }⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ toEnd R (Module.End R M) M = LieHom.id

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
⊢ ∃ x ∈ N, I x ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsFaithful R L M
x : L
⊢ (toEnd R L M) x = 0 ↔ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : IsFaithful R L M
x : L
hx : ∀ (m : M), ⁅x, m⁆ = 0
⊢ (toEnd R L M) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝ : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
⊢ I x = N

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ IsFaithful R L M ↔ ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
⊢ IsNilpotent (Ring.jacobson R)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsFaithful R L M
L' : LieSubalgebra R L
⊢ IsFaithful R (↥L') M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ Injective ⇑(toEnd R (Module.End R M) M)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
hx : x ∈ (Submodule.toAddSubmonoid 0).carrier
_hy : y ∈ (Submodule.toAddSubmonoid 0).carrier
⊢ ⁅x, y⁆ ∈ (Submodule.toAddSubmonoid 0).carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : CommMagma A
inst✝ : IsCommJordan A
a b : A
⊢ a * b * a = a * (b * a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : CommMagma A
inst✝ : IsCommJordan A
a b : A
⊢ a * a * (a * b) = a * (a * a * b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : CommMagma A
inst✝ : IsCommJordan A
a b : A
⊢ a * a * (b * a) = a * a * b * a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : CommMagma A
inst✝ : IsCommJordan A
a b : A
⊢ b * a * (a * a) = b * (a * a) * a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * b * a = a * (b * a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * a * (a * b) = a * (a * a * b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * a * (b * a) = a * a * b * a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * b * (a * a) = a * (b * (a * a))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ b * a * (a * a) = b * (a * a) * a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
y : ↥N
n : ℕ
⊢ ↑(((toEnd R L ↥N) x ^ n) y) = ((toEnd R L M) x ^ n) ↑y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' L'' : LieSubalgebra R L
h : (fun L' ↦ L'.carrier) L' = (fun L' ↦ L'.carrier) L''
⊢ L' = L''

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (x y z : ↥L'), ⟨⁅↑(x + y), ↑z⁆, ⋯⟩ = ⟨⁅↑x, ↑z⁆, ⋯⟩ + ⟨⁅↑y, ↑z⁆, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
z : M
⊢ (φ x) ⁅y, z⁆ = ⁅((ad R L) x) y, z⁆ + ⁅y, (φ x) z⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (x y z : ↥L'), ⟨⁅↑x, ↑(y + z)⁆, ⋯⟩ = ⟨⁅↑x, ↑y⁆, ⋯⟩ + ⟨⁅↑x, ↑z⁆, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (x : ↥L'), ⟨⁅↑x, ↑x⁆, ⋯⟩ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (x y z : ↥L'), ⟨⁅↑x, ↑⟨⁅↑y, ↑z⁆, ⋯⟩⁆, ⋯⟩ = ⟨⁅↑⟨⁅↑x, ↑y⁆, ⋯⟩, ↑z⁆, ⋯⟩ + ⟨⁅↑y, ↑⟨⁅↑x, ↑z⁆, ⋯⟩⁆, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
this : 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0
⊢ 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) = ⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (t : R) (x y : ↥L'), ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L' : LieSubalgebra R L
⊢ ∀ (t : R) (x y : ↥L'), ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
by
    { intros
      apply SetCoe.ext
      apply lie_smul }

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
L₁' L₂' : LieSubalgebra R L
h : L₁'.toSubmodule = L₂'.toSubmodule
⊢ L₁' = L₂'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
⊢ 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) = ⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
L' : LieSubalgebra R L
M : Type w
inst✝⁶ : AddCommGroup M
inst✝⁵ : LieRingModule L M
N : Type w₁
inst✝⁴ : AddCommGroup N
inst✝³ : LieRingModule L N
inst✝² : Module R N
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : ↥L'
m : M
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
L' : LieSubalgebra R L
M : Type w
inst✝⁶ : AddCommGroup M
inst✝⁵ : LieRingModule L M
N : Type w₁
inst✝⁴ : AddCommGroup N
inst✝³ : LieRingModule L N
inst✝² : Module R N
inst✝¹ : Module R M
inst✝ : LieModule R L M
t : R
x : ↥L'
m : M
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
⊢ ∀ {x y : L₂}, x ∈ (↑f).range.carrier → y ∈ (↑f).range.carrier → ⁅x, y⁆ ∈ (↑f).range.carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x y : L
⊢ (↑f).rangeRestrict.toFun ⁅x, y⁆ = ⁅(↑f).rangeRestrict.toFun x, (↑f).rangeRestrict.toFun y⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
⊢ Function.Surjective ⇑f.rangeRestrict

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
h : Function.Injective ⇑f
x y : L
hxy : f.rangeRestrict x = f.rangeRestrict y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (∃ K, K.toSubmodule = p) ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
⊢ K.incl.range = K

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x y : L₂
hx : x ∈ (Submodule.map (↑f) K.toSubmodule).carrier
hy : y ∈ (Submodule.map (↑f) K.toSubmodule).carrier
⊢ ⁅x, y⁆ ∈ (Submodule.map (↑f) K.toSubmodule).carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x y : L
hx : x ∈ (Submodule.comap (↑f) K₂.toSubmodule).carrier
hy : y ∈ (Submodule.comap (↑f) K₂.toSubmodule).carrier
this : ⁅f x, f y⁆ ∈ K₂
⊢ ⁅x, y⁆ ∈ (Submodule.comap (↑f) K₂.toSubmodule).carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x y : L
hx : x ∈ (Submodule.comap (↑f) K₂.toSubmodule).carrier
hy : y ∈ (Submodule.comap (↑f) K₂.toSubmodule).carrier
⊢ ⁅f x, f y⁆ ∈ K₂

Tactic:
exact K₂.lie_mem hx hy

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x y : L
hx : x ∈ (Submodule.comap (↑f) K₂.toSubmodule).carrier
hy : y ∈ (Submodule.comap (↑f) K₂.toSubmodule).carrier
⊢ ⁅x, y⁆ ∈ (Submodule.comap (↑f) K₂.toSubmodule).carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
hf : Function.Injective ⇑f
x y : ↥K
⊢ (↑(Submodule.equivMapOfInjective (↑f) hf K.toSubmodule)).toFun ⁅x, y⁆ =
    ⁅(↑(Submodule.equivMapOfInjective (↑f) hf K.toSubmodule)).toFun x,
      (↑(Submodule.equivMapOfInjective (↑f) hf K.toSubmodule)).toFun y⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
⊢ K.toSubmodule = ⊥ ↔ K = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
⊢ K.toSubmodule = ⊤ ↔ K = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
⊢ f.range = map f ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : 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 : x ∈ (sInf {x | ∃ s ∈ S, s.toSubmodule = x}).carrier
hy : y ∈ (sInf {x | ∃ s ∈ S, s.toSubmodule = x}).carrier
⊢ ⁅x, y⁆ ∈ (sInf {x | ∃ s ∈ S, s.toSubmodule = x}).carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
⊢ ↑(sInf S) = ⋂ s ∈ S, ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
⊢ ∀ (K K' : LieSubalgebra R L), ↑K ⊆ ↑K' ↔ K ≤ K'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
S : Set (LieSubalgebra R L)
⊢ IsGLB S (sInf S)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
N : LieSubalgebra R L
x✝ : L
h : x✝ ∈ ⊥
⊢ x✝ ∈ N

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
z : M
n : ℕ
⊢ (φ x ^ n) ⁅y, z⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L) x ^ ij.1) y, (φ x ^ ij.2) z⁆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
M₂ : Type w₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
x : L
⊢ ((toEnd R L M₂) x ^ k) ∘ₗ ↑f = ↑f ∘ₗ (toEnd R L M) x ^ k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
⊢ Submodule.map ((toEnd R L M) x) ↑N ≤ ↑N

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
x : L
⊢ x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
m : M
hm : m ∈ ↑N
⊢ ((toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑N

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
⊢ K = ⊥ ↔ ∀ x ∈ K, x = 0

Tactic:
by

Goal state after: