mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
⊢ ∀ (m : R) (x : A ⊗[R] L), (LinearMap.rTensor L ↑d) (m • x) = (RingHom.id R) m • (LinearMap.rTensor L ↑d) x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
⊢ (LinearMap.rTensor L ↑d) ⁅0, y⁆ = ⁅0, (LinearMap.rTensor L ↑d) y⁆ - ⁅y, (LinearMap.rTensor L ↑d) 0⁆

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : Derivation R A A
x y : A ⊗[R] L
x✝ : A
l : L
⊢ (LinearMap.rTensor L ↑d) ⁅x✝ ⊗ₜ[R] l, 0⁆ =
    ⁅x✝ ⊗ₜ[R] l, (LinearMap.rTensor L ↑d) 0⁆ - ⁅0, (LinearMap.rTensor L ↑d) (x✝ ⊗ₜ[R] l)⁆

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝¹ x✝ : Derivation R A A
a✝ : A ⊗[R] L
⊢ { toFun := ⇑(LinearMap.rTensor L ↑(x✝¹ + x✝)), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } a✝ =
    ({ toFun := ⇑(LinearMap.rTensor L ↑x✝¹), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } +
        { toFun := ⇑(LinearMap.rTensor L ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ })
      a✝

Tactic:
simp

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

Goal state before:
pp: case zero
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : z ∈ engel K ↑v
z' : Q := (LieSubmodule.Quotient.mk' E) z
hz' : ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0
n : ℕ := Nat.find hz'
_hn : n = Nat.find hz'
hn : ((toEnd K (↥U) Q) v ^ n) z' = 0
⊢ 0 = 0 ∨ ∃ k, 0 = k + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝¹ : R
x✝ : Derivation R A A
a✝ : A ⊗[R] L
⊢ { toFun := ⇑(LinearMap.rTensor L ↑(x✝¹ • x✝)), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } a✝ =
    ((RingHom.id R) x✝¹ • { toFun := ⇑(LinearMap.rTensor L ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }) a✝

Tactic:
simp

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

Goal state before:
pp: case succ
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : z ∈ engel K ↑v
z' : Q := (LieSubmodule.Quotient.mk' E) z
hz' : ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0
n : ℕ := Nat.find hz'
_hn : n = Nat.find hz'
hn : ((toEnd K (↥U) Q) v ^ n) z' = 0
n✝ : ℕ
⊢ n✝ + 1 = 0 ∨ ∃ k, n✝ + 1 = k + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝¹ x✝ : Derivation R A A
z : A ⊗[R] L
⊢ { toFun := ⇑(LinearMap.rTensor L ↑⁅x✝¹, x✝⁆), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } 0 =
    ⁅{ toFun := ⇑(LinearMap.rTensor L ↑x✝¹), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ },
        { toFun := ⇑(LinearMap.rTensor L ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }⁆
      0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
⊢ ∀ (x y : A ⊗[R] L), (LinearMap.lTensor A ↑d) (x + y) = (LinearMap.lTensor A ↑d) x + (LinearMap.lTensor A ↑d) y

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
⊢ ∀ (m : R) (x : A ⊗[R] L), (LinearMap.lTensor A ↑d) (m • x) = (RingHom.id R) m • (LinearMap.lTensor A ↑d) x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
⊢ (LinearMap.lTensor A ↑d) ⁅0, y⁆ = ⁅0, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) 0⁆

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
d : LieDerivation R L L
x y : A ⊗[R] L
x✝ : A
y✝ : L
⊢ (LinearMap.lTensor A ↑d) ⁅x✝ ⊗ₜ[R] y✝, 0⁆ =
    ⁅x✝ ⊗ₜ[R] y✝, (LinearMap.lTensor A ↑d) 0⁆ - ⁅0, (LinearMap.lTensor A ↑d) (x✝ ⊗ₜ[R] y✝)⁆

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u
ι : Type v
inst✝⁷ : CommRing R
L : Type w₁
M : ι → Type w
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : (i : ι) → AddCommGroup (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → LieRingModule L (M i)
inst✝¹ : ∀ (i : ι), LieModule R L (M i)
inst✝ : DecidableEq ι
j : ι
x : L
m : M j
i : ι
h : j = i
⊢ ((lof R ι M j).toFun ⁅x, m⁆) j = ⁅x, (lof R ι M j).toFun m⁆ j

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝¹ x✝ : LieDerivation R L L
a✝ : A ⊗[R] L
⊢ { toFun := ⇑(LinearMap.lTensor A ↑(x✝¹ + x✝)), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } a✝ =
    ({ toFun := ⇑(LinearMap.lTensor A ↑x✝¹), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } +
        { toFun := ⇑(LinearMap.lTensor A ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ })
      a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝¹ : R
x✝ : LieDerivation R L L
a✝ : A ⊗[R] L
⊢ { toFun := ⇑(LinearMap.lTensor A ↑(x✝¹ • x✝)), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } a✝ =
    ((RingHom.id R) x✝¹ • { toFun := ⇑(LinearMap.lTensor A ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝¹ x✝ : LieDerivation R L L
z : A ⊗[R] L
⊢ { toFun := ⇑(LinearMap.lTensor A ↑⁅x✝¹, x✝⁆), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } 0 =
    ⁅{ toFun := ⇑(LinearMap.lTensor A ↑x✝¹), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ },
        { toFun := ⇑(LinearMap.lTensor A ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }⁆
      0

Tactic:
simp

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

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁵ : CommRing R
L : ι → Type w
inst✝⁴ : (i : ι) → LieRing (L i)
inst✝³ : (i : ι) → LieAlgebra R (L i)
inst✝² : DecidableEq ι
L' : Type w₁
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : (i : ι) → L i →ₗ⁅R⁆ L'
hf : Pairwise fun i j ↦ ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0
y✝ : ⨁ (i : ι), L i
f' : (i : ι) → L i →ₗ[R] L' := fun i ↦ ↑(f i)
this :
  ∀ (i j : ι) (y : L i) (x : L j),
    (toModule R ι L' f') ⁅(of L j) x, (of L i) y⁆ =
      ⁅(toModule R ι L' f') ((of L j) x), (toModule R ι L' f') ((of L i) y)⁆
i : ι
y : L i
j : ι
x : L j
⊢ ((toModule R ι L' f' ∘ₗ (LieAlgebra.ad R (⨁ (i : ι), L i)) ((of L i) y)) ∘ₗ lof R ι L j) x =
    (((LieAlgebra.ad R L') ((toModule R ι L' f') ((of L i) y)) ∘ₗ toModule R ι L' f') ∘ₗ lof R ι L j) x

Tactic:
exact this j i x y

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝ : X
⊢ (⇑(((UniversalEnvelopingAlgebra.lift R) ((lift R) (FreeAlgebra.ι R))).comp
            ((FreeAlgebra.lift R) (⇑(UniversalEnvelopingAlgebra.ι R) ∘ of R))) ∘
        FreeAlgebra.ι R)
      x✝ =
    (⇑(AlgHom.id R (FreeAlgebra R X)) ∘ FreeAlgebra.ι R) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝ : X
⊢ ((((FreeAlgebra.lift R) (⇑(UniversalEnvelopingAlgebra.ι R) ∘ of R)).comp
              ((UniversalEnvelopingAlgebra.lift R) ((lift R) (FreeAlgebra.ι R)))).toLieHom.comp
        (UniversalEnvelopingAlgebra.ι R))
      (of R x✝) =
    ((AlgHom.id R (UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))).toLieHom.comp (UniversalEnvelopingAlgebra.ι R))
      (of R x✝)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x✝² x✝¹ x✝ : ⨁ (i : ι), ↥(ℒ i)
⊢ (decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm (x✝² + x✝¹), (decomposeLinearEquiv ℒ).symm x✝⁆ =
    (decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝², (decomposeLinearEquiv ℒ).symm x✝⁆ +
      (decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝¹, (decomposeLinearEquiv ℒ).symm x✝⁆

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x✝² x✝¹ x✝ : ⨁ (i : ι), ↥(ℒ i)
⊢ (decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝², (decomposeLinearEquiv ℒ).symm (x✝¹ + x✝)⁆ =
    (decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝², (decomposeLinearEquiv ℒ).symm x✝¹⁆ +
      (decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝², (decomposeLinearEquiv ℒ).symm x✝⁆

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x✝ : ⨁ (i : ι), ↥(ℒ i)
⊢ (decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝, (decomposeLinearEquiv ℒ).symm x✝⁆ = 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x✝² x✝¹ x✝ : ⨁ (i : ι), ↥(ℒ i)
⊢ (decomposeLinearEquiv ℒ)
      ⁅(decomposeLinearEquiv ℒ).symm x✝²,
        (decomposeLinearEquiv ℒ).symm
          ((decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝¹, (decomposeLinearEquiv ℒ).symm x✝⁆)⁆ =
    (decomposeLinearEquiv ℒ)
        ⁅(decomposeLinearEquiv ℒ).symm
            ((decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝², (decomposeLinearEquiv ℒ).symm x✝¹⁆),
          (decomposeLinearEquiv ℒ).symm x✝⁆ +
      (decomposeLinearEquiv ℒ)
        ⁅(decomposeLinearEquiv ℒ).symm x✝¹,
          (decomposeLinearEquiv ℒ).symm
            ((decomposeLinearEquiv ℒ) ⁅(decomposeLinearEquiv ℒ).symm x✝², (decomposeLinearEquiv ℒ).symm x✝⁆)⁆

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x y : L
⊢ (decomposeLinearEquiv ℒ) ⁅x, y⁆ = ⁅(decomposeLinearEquiv ℒ) x, (decomposeLinearEquiv ℒ) y⁆

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x y : ⨁ (i : ι), ↥(ℒ i)
⊢ (decomposeLinearEquiv ℒ).symm ⁅x, y⁆ = ⁅(decomposeLinearEquiv ℒ).symm x, (decomposeLinearEquiv ℒ).symm y⁆

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x✝ : ⨁ (i : ι), ↥(ℒ i)
⊢ 0 • x✝ = 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
x✝² : R
x✝¹ x✝ : ⨁ (i : ι), ↥(ℒ i)
⊢ ⁅x✝¹, x✝² • x✝⁆ = x✝² • ⁅x✝¹, x✝⁆

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
⊢ ∀ {x y : L},
    (↑(decomposeLinearEquiv ℒ)).toFun ⁅x, y⁆ =
      ⁅(↑(decomposeLinearEquiv ℒ)).toFun x, (↑(decomposeLinearEquiv ℒ)).toFun y⁆

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
i : ι
⊢ φ i ∈ Set.center R

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
x y : ⨁ (i : ι), ↥(ℒ i)
k : ι
w✝ : ↥(ℒ k)
hb : (decompose ℒ).symm ((lof R ι (fun x ↦ ↥(ℒ x)) k) w✝) ∈ ℒ k
⊢ (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id))
      ((lof R ι (fun x ↦ ↥(ℒ x)) k) w✝) =
    φ k • (lof R ι (fun x ↦ ↥(ℒ x)) k) w✝

Tactic:
simp

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

Goal state before:
pp: case h0
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
y : ⨁ (i : ι), ↥(ℒ i)
hM :
  ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i)),
    (decompose ℒ).symm b ∈ ℒ k →
      (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) b = φ k • b
j : ι
⊢ ↑(((toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft (φ i) ⋯) ⁅0, y⁆) j) =
    ↑((⁅0, (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft (φ i) ⋯) y⁆ -
          ⁅y, (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft (φ i) ⋯) 0⁆)
        j)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: case e_3
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ f (Multiplicative.toAdd 1) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: case e_4.e_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ (fun x ↦ x ∈ gradeBy R (⇑f) (f (Multiplicative.toAdd 1))) = fun x ↦ x ∈ gradeBy R (⇑f) 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: case e_4.e_4
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
⊢ ⋯ ≍ ⋯

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
y : ⨁ (i : ι), ↥(ℒ i)
hM :
  ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i)),
    (decompose ℒ).symm b ∈ ℒ k →
      (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) b = φ k • b
j i : ι
a : ↥(ℒ i)
f : ⨁ (i : ι), ↥(ℒ i)
a✝¹ : f i = 0
a✝ : a ≠ 0
ih :
  ↑(((toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) ⁅f, y⁆) j) =
    ↑(⁅f, (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) y⁆ j) -
      ↑(⁅y, (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) f⁆ j)
⊢ (decompose ℒ).symm ((of (fun x ↦ ↥(ℒ x)) i) a) ∈ ℒ i

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : LieRing N
inst✝³ : LieAlgebra R N
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
i : N →ₗ⁅R⁆ L
p : L →ₗ⁅R⁆ M
inst✝ : IsExtension i p
⊢ (LieIdeal.toLieSubalgebra R L p.ker).toSubmodule = i.range.toSubmodule

Tactic:
simp [exact (i := i) (p := p)]

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

Goal state before:
pp: case hadd.h0
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
hM :
  ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i)),
    (decompose ℒ).symm b ∈ ℒ k →
      (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) b = φ k • b
j i : ι
a : ↥(ℒ i)
f : ⨁ (i : ι), ↥(ℒ i)
a✝¹ : f i = 0
a✝ : a ≠ 0
⊢ ↑(((toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id))
          ⁅(of (fun i ↦ ↥(ℒ i)) i) a, 0⁆)
        j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a,
            (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) 0⁆
          j) -
      ↑(⁅0, φ i • (of (fun x ↦ ↥(ℒ x)) i) a⁆ j)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
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
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ (ofProd c)
      (⁅((ofProd c).symm (x + y)).1, ((ofProd c).symm z).1⁆,
        (↑↑c ((ofProd c).symm (x + y)).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm (x + y)).1, ((ofProd c).symm z).2⁆ -
          ⁅((ofProd c).symm z).1, ((ofProd c).symm (x + y)).2⁆) =
    (ofProd c)
        (⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆,
          (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ -
            ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆) +
      (ofProd c)
        (⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆,
          (↑↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆ -
            ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆)

Tactic:
← of_add

Goal state after:
R : Type u_1
N : Type u_2
L : Type u_3
M : Type u_4
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
c : ↥(twoCocycle R L M)
x y z : ofTwoCocycle c
⊢ (ofProd c)
      (⁅((ofProd c).symm (x + y)).1, ((ofProd c).symm z).1⁆,
        (↑↑c ((ofProd c).symm (x + y)).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm (x + y)).1, ((ofProd c).symm z).2⁆ -
          ⁅((ofProd c).symm z).1, ((ofProd c).symm (x + y)).2⁆) =
    (ofProd c)
      ((⁅((ofProd c).symm x).1, ((ofProd c).symm z).1⁆,
          (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆ -
            ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆) +
        (⁅((ofProd c).symm y).1, ((ofProd c).symm z).1⁆,
          (↑↑c ((ofProd c).symm y).1) ((ofProd c).symm z).1 + ⁅((ofProd c).symm y).1, ((ofProd c).symm z).2⁆ -
            ⁅((ofProd c).symm z).1, ((ofProd c).symm y).2⁆))