mathlib-initiative/mathlib-tactics huggingface dataset:
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).1, ((ofProd c).symm (y + z)).1⁆,
        (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm (y + z)).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm (y + z)).2⁆ -
          ⁅((ofProd c).symm (y + z)).1, ((ofProd c).symm x).2⁆) =
    (ofProd c)
        (⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆,
          (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆ -
            ⁅((ofProd c).symm y).1, ((ofProd c).symm x).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⁆)

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).1, ((ofProd c).symm (y + z)).1⁆,
        (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm (y + z)).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm (y + z)).2⁆ -
          ⁅((ofProd c).symm (y + z)).1, ((ofProd c).symm x).2⁆) =
    (ofProd c)
      ((⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆,
          (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆ -
            ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆) +
        (⁅((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⁆))
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).symm x).1, ((ofProd c).symm (y + z)).1⁆,
      (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm (y + z)).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm (y + z)).2⁆ -
        ⁅((ofProd c).symm (y + z)).1, ((ofProd c).symm x).2⁆) =
    (⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆,
        (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆ -
          ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆) +
      (⁅((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⁆)

Tactic:
simp

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
⊢ (↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1 + (↑c ((ofProd c).symm x).1) ((ofProd c).symm z).1 +
        (⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆ + ⁅((ofProd c).symm x).1, ((ofProd c).symm z).2⁆) -
      (⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆ + ⁅((ofProd c).symm z).1, ((ofProd c).symm x).2⁆) =
    (↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆ -
        ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆ +
      ((↑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⁆)
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
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
k : ι
b : ↥(ℒ k)
f : ⨁ (i : ι), ↥(ℒ i)
a✝¹ : f k = 0
a✝ : b ≠ 0
ih :
  ↑(((toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id))
          ⁅(of (fun i ↦ ↥(ℒ i)) i) a, f⁆)
        j) =
    ↑(⁅(of (fun i ↦ ↥(ℒ i)) i) a,
            (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) f⁆
          j) -
      ↑(⁅f, φ i • (of (fun x ↦ ↥(ℒ x)) i) a⁆ j)
this : (decompose ℒ).symm ⁅(of (fun i ↦ ↥(ℒ i)) i) a, (of (fun i ↦ ↥(ℒ i)) k) b⁆ ∈ ℒ (i + k)
⊢ (decompose ℒ).symm ((of (fun x ↦ ↥(ℒ x)) k) b) ∈ ℒ k

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 : ofTwoCocycle c
⊢ (⁅((ofProd c).symm x).1, ((ofProd c).symm x).1⁆,
      0 + ⁅((ofProd c).symm x).1, ((ofProd c).symm x).2⁆ - ⁅((ofProd c).symm x).1, ((ofProd c).symm x).2⁆) =
    0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
i✝ : ι
x✝ : ↥(ℳ i✝)
⊢ ((AlgebraTensorModule.curry
            (((coeLinearMap fun i ↦ Submodule.baseChange S (ℳ i)) ∘ₗ lmap fun x ↦ Submodule.toBaseChange S (ℳ x)) ∘ₗ
              ↑(directSumRight R S S fun i ↦ ↥(ℳ i))))
          1 ∘ₗ
        lof R ι (fun i ↦ ↥(ℳ i)) i✝)
      x✝ =
    ((AlgebraTensorModule.curry
            (LinearMap.id ∘ₗ ↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ)).symm))
          1 ∘ₗ
        lof R ι (fun i ↦ ↥(ℳ i)) i✝)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
S : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : Decomposition ℳ
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
i✝ : ι
x✝ : ↥(ℳ i✝)
⊢ ((AlgebraTensorModule.curry
          (((((lmap fun x ↦ Submodule.toBaseChange S (ℳ x)) ∘ₗ
                  ↑(directSumRight R S S fun i ↦ ↥(ℳ i)) ∘ₗ
                    ↑(LinearEquiv.baseChange R S M (⨁ (i : ι), ↥(ℳ i)) (decomposeLinearEquiv ℳ))) ∘ₗ
                coeLinearMap fun i ↦ Submodule.baseChange S (ℳ i)) ∘ₗ
              lof S ι (fun i ↦ ↥(Submodule.baseChange S (ℳ i))) i✝) ∘ₗ
            Submodule.toBaseChange S (ℳ i✝)))
        1)
      x✝ =
    ((AlgebraTensorModule.curry
          ((LinearMap.id ∘ₗ lof S ι (fun i ↦ ↥(Submodule.baseChange S (ℳ i))) i✝) ∘ₗ Submodule.toBaseChange S (ℳ i✝)))
        1)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
x✝¹ : ↥(ℳ i)
x✝ : N
⊢ ((AlgebraTensorModule.curry
          (rTensor N (component R ι (fun i ↦ ↥(ℳ i)) i ∘ₗ ↑(decomposeLinearEquiv ℳ)) ∘ₗ rTensor N (ℳ i).subtype))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry LinearMap.id) x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ℳ : ι → Submodule R M
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
i : ι
x✝ : ↥(ℳ i)
i✝ : ι
⊢ ↑(((↑(decomposeLinearEquiv ℳ) ∘ₗ (ℳ i).subtype) x✝) i✝) = ↑(((lof R ι (fun i ↦ ↥(ℳ i)) i) x✝) i✝)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Decomposition

Goal state before:
pp: case zero
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ℳ : ι → Submodule R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Decomposition ℳ
⊢ (LinearEquiv.rTensor N (decomposeLinearEquiv ℳ)) ((DirectSum.coeAddMonoidHom (decomposeTensor ℳ N)) 0) =
    (directSumLeft R R (fun i ↦ ↥(ℳ i)) N).symm ((congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm 0)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
n : ℕ
hn :
  ∀ (w : A),
    ∀ a < n + 1, (T χ w) (((toEnd R L V) z ^ a) v) ∈ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}
w : A
hm : n + 1 < n + 1 + 1
⊢ ∀ (w : A), ⁅w, ((toEnd R L V) z ^ n) v⁆ = (T χ w) (((toEnd R L V) z ^ n) v) + χ w • ((toEnd R L V) z ^ n) v

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✝¹ x✝ : L
⊢ (decomposeLinearEquiv ℒ).symm ((ofGradingSum ℒ φ) ((decomposeLinearEquiv ℒ) (x✝¹ + x✝))) =
    (decomposeLinearEquiv ℒ).symm ((ofGradingSum ℒ φ) ((decomposeLinearEquiv ℒ) x✝¹)) +
      (decomposeLinearEquiv ℒ).symm ((ofGradingSum ℒ φ) ((decomposeLinearEquiv ℒ) 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 ℒ
φ : ι →+ R
x✝¹ : R
x✝ : L
⊢ (decomposeLinearEquiv ℒ).symm ((ofGradingSum ℒ φ) ((decomposeLinearEquiv ℒ) (x✝¹ • x✝))) =
    (RingHom.id R) x✝¹ • (decomposeLinearEquiv ℒ).symm ((ofGradingSum ℒ φ) ((decomposeLinearEquiv ℒ) x✝))

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝² + x✝¹, x✝⁆ = ⁅x✝², x✝⁆ + ⁅x✝¹, x✝⁆

Tactic:
simp

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝².left, x✝.left⁆ + ⁅x✝¹.left, x✝.left⁆ + ((ψ x✝².right) x✝.left + (ψ x✝¹.right) x✝.left) -
      ((ψ x✝.right) x✝².left + (ψ x✝.right) x✝¹.left) =
    ⁅x✝².left, x✝.left⁆ + (ψ x✝².right) x✝.left - (ψ x✝.right) x✝².left +
      (⁅x✝¹.left, x✝.left⁆ + (ψ x✝¹.right) x✝.left - (ψ x✝.right) x✝¹.left)
Module: Mathlib.Algebra.Lie.SemiDirect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝², x✝¹ + x✝⁆ = ⁅x✝², x✝¹⁆ + ⁅x✝², x✝⁆

Tactic:
simp

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝².left, x✝¹.left⁆ + ⁅x✝².left, x✝.left⁆ + ((ψ x✝².right) x✝¹.left + (ψ x✝².right) x✝.left) -
      ((ψ x✝¹.right) x✝².left + (ψ x✝.right) x✝².left) =
    ⁅x✝².left, x✝¹.left⁆ + (ψ x✝².right) x✝¹.left - (ψ x✝¹.right) x✝².left +
      (⁅x✝².left, x✝.left⁆ + (ψ x✝².right) x✝.left - (ψ x✝.right) x✝².left)
Module: Mathlib.Algebra.Lie.SemiDirect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝, x✝⁆ = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝², ⁅x✝¹, x✝⁆⁆ = ⁅⁅x✝², x✝¹⁆, x✝⁆ + ⁅x✝¹, ⁅x✝², x✝⁆⁆

Tactic:
simp

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝² x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ ⁅x✝².left, ⁅x✝¹.left, x✝.left⁆⁆ + ⁅x✝².left, (ψ x✝¹.right) x✝.left⁆ - ⁅x✝².left, (ψ x✝.right) x✝¹.left⁆ +
        (⁅x✝¹.left, (ψ x✝².right) x✝.left⁆ - ⁅x✝.left, (ψ x✝².right) x✝¹.left⁆ + (ψ x✝².right) ((ψ x✝¹.right) x✝.left) -
          (ψ x✝².right) ((ψ x✝.right) x✝¹.left)) -
      ((ψ x✝¹.right) ((ψ x✝.right) x✝².left) - (ψ x✝.right) ((ψ x✝¹.right) x✝².left)) =
    ⁅x✝².left, ⁅x✝¹.left, x✝.left⁆⁆ - ⁅x✝¹.left, ⁅x✝².left, x✝.left⁆⁆ + ⁅(ψ x✝².right) x✝¹.left, x✝.left⁆ -
            ⁅(ψ x✝¹.right) x✝².left, x✝.left⁆ +
          ((ψ x✝².right) ((ψ x✝¹.right) x✝.left) - (ψ x✝¹.right) ((ψ x✝².right) x✝.left)) -
        (⁅x✝².left, (ψ x✝.right) x✝¹.left⁆ - ⁅x✝¹.left, (ψ x✝.right) x✝².left⁆ + (ψ x✝.right) ((ψ x✝².right) x✝¹.left) -
          (ψ x✝.right) ((ψ x✝¹.right) x✝².left)) +
      (⁅x✝¹.left, ⁅x✝².left, x✝.left⁆⁆ + ⁅x✝¹.left, (ψ x✝².right) x✝.left⁆ - ⁅x✝¹.left, (ψ x✝.right) x✝².left⁆ +
          (⁅x✝².left, (ψ x✝¹.right) x✝.left⁆ - ⁅x✝.left, (ψ x✝¹.right) x✝².left⁆ +
              (ψ x✝¹.right) ((ψ x✝².right) x✝.left) -
            (ψ x✝¹.right) ((ψ x✝.right) x✝².left)) -
        ((ψ x✝².right) ((ψ x✝.right) x✝¹.left) - (ψ x✝.right) ((ψ x✝².right) x✝¹.left)))
Module: Mathlib.Algebra.Lie.SemiDirect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝¹ x✝ : K
⊢ { left := x✝¹ + x✝, right := 0 } = { left := x✝¹, right := 0 } + { left := x✝, right := 0 }

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝¹ : R
x✝ : K
⊢ { left := x✝¹ • x✝, right := 0 } = (RingHom.id R) x✝¹ • { left := x✝, right := 0 }

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
⊢ ∀ {x y : K}, { left := ⁅x, y⁆, right := 0 } = ⁅{ left := x, right := 0 }, { left := y, right := 0 }⁆

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝¹ x✝ : L
⊢ { left := 0, right := x✝¹ + x✝ } = { left := 0, right := x✝¹ } + { left := 0, right := x✝ }

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝¹ : R
x✝ : L
⊢ { left := 0, right := x✝¹ • x✝ } = (RingHom.id R) x✝¹ • { left := 0, right := x✝ }

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
⊢ ∀ {x y : L}, { left := 0, right := ⁅x, y⁆ } = ⁅{ left := 0, right := x }, { left := 0, right := y }⁆

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ (x✝¹ + x✝).right = x✝¹.right + x✝.right

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝¹ : R
x✝ : K ⋊⁅ψ⁆ L
⊢ (x✝¹ • x✝).right = (RingHom.id R) x✝¹ • x✝.right

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
⊢ ∀ {x y : K ⋊⁅ψ⁆ L}, ⁅x, y⁆.right = ⁅x.right, y.right⁆

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝¹ x✝ : K ⋊⁅ψ⁆ L
⊢ (x✝¹ + x✝).left = x✝¹.left + x✝.left

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x✝¹ : R
x✝ : K ⋊⁅ψ⁆ L
⊢ (x✝¹ • x✝).left = (RingHom.id R) x✝¹ • x✝.left

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x : K
⊢ (projr ψ) ((inl ψ) x) = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x : L
⊢ (projr ψ) ((inr ψ) x) = x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x : L
⊢ (projl ψ) ((inr ψ) x) = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
ψ : L →ₗ⁅R⁆ LieDerivation R K K
x : K
⊢ (projl ψ) ((inl ψ) x) = x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : LieRing K
inst✝² : LieAlgebra R K
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x✝¹ x✝ : K ⋊⁅0⁆ L
⊢ (↑(toProdl 0)).toFun ⁅x✝¹, x✝⁆ = ⁅(↑(toProdl 0)).toFun x✝¹, (↑(toProdl 0)).toFun x✝⁆

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 c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h : ↑c' = ↑c + (d₁₂ R L M) x
y : ofTwoCocycle c
⊢ (fun z ↦ (ofProd c) (((ofProd c').symm z).1, ((ofProd c').symm z).2 + x ((ofProd c').symm z).1))
      ((fun y ↦ (ofProd c') (((ofProd c).symm y).1, ((ofProd c).symm y).2 - x ((ofProd c).symm y).1)) y) =
    y

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 c' : ↥(twoCocycle R L M)
x : oneCochain R L M
h : ↑c' = ↑c + (d₁₂ R L M) x
z : ofTwoCocycle c'
⊢ (fun y ↦ (ofProd c') (((ofProd c).symm y).1, ((ofProd c).symm y).2 - x ((ofProd c).symm y).1))
      ((fun z ↦ (ofProd c) (((ofProd c').symm z).1, ((ofProd c').symm z).2 + x ((ofProd c').symm z).1)) z) =
    z

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 M
inst✝³ : LieAlgebra R M
inst✝² : IsLieAbelian M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x✝¹ x✝ : LieAlgebra.ofTwoCocycle c
⊢ ((ofProd c).symm (x✝¹ + x✝)).1 = ((ofProd c).symm x✝¹).1 + ((ofProd c).symm x✝).1

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 M
inst✝³ : LieAlgebra R M
inst✝² : IsLieAbelian M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x✝¹ : R
x✝ : LieAlgebra.ofTwoCocycle c
⊢ ((ofProd c).symm (x✝¹ • x✝)).1 = (RingHom.id R) x✝¹ • ((ofProd c).symm x✝).1

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 M
inst✝³ : LieAlgebra R M
inst✝² : IsLieAbelian M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x y : M
⊢ { toFun := fun x ↦ (ofProd c) (0, x), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } x =
      { toFun := fun x ↦ (ofProd c) (0, x), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } y →
    x = y

Tactic:
simp

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

Goal state before:
pp: case h
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 M
inst✝³ : LieAlgebra R M
inst✝² : IsLieAbelian M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
c : ↥(twoCocycle R L M)
x : L
⊢ { toFun := fun x ↦ ((ofProd c).symm x).1, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ } ((ofProd c) (x, 0)) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Lie.Semisimple.Lemmas

Goal state before:
pp: case zero
L : Type u_2
M : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
R : Type u_4
inst✝³ : CommRing R
inst✝² : LieAlgebra R L
inst✝¹ : Module R M
inst✝ : LieModule R L M
s : Set L
hs : ∀ x ∈ s, (trace R M) ((toEnd R L M) x) = 0
x : L
⊢ (trace R M) ((toEnd R L M) 0) = 0

Tactic:
simp

Goal state after: