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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_2
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
f : oneCochain R L M
x : L
⊢ ({ toFun := fun x ↦ { toFun := fun y ↦ ⁅x, f y⁆ - ⁅y, f x⁆ - f ⁅x, y⁆, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
          map_smul' := ⋯ }
        x)
      x =
    0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst✝³ : CommRing A'
inst✝² : Algebra R A'
inst✝¹ : Algebra A A'
inst✝ : IsScalarTower R A A'
⊢ 0 ∈ {x | (compAlgebraMapL R A A' A') x.1 = (Algebra.ofId A A').toLinearMap.compDer x.2}

Tactic:
by 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) (x + y) = (LinearMap.rTensor L ↑d) x + (LinearMap.rTensor L ↑d) y

Tactic:
by 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
⊢ ∀ (m : R) (x : A ⊗[R] L), (LinearMap.rTensor L ↑d) (m • x) = (RingHom.id R) m • (LinearMap.rTensor L ↑d) x

Tactic:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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⁆ = ⁅x, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) x⁆

Tactic:
refine x.induction_on (by simp) ?_ ?_

Goal state after:
case refine_1
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_1 : L),
    (LinearMap.lTensor A ↑d) ⁅x ⊗ₜ[R] y_1, y⁆ =
      ⁅x ⊗ₜ[R] y_1, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) (x ⊗ₜ[R] y_1)⁆

case refine_2
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 y_1 : A ⊗[R] L),
    (LinearMap.lTensor A ↑d) ⁅x, y⁆ = ⁅x, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) x⁆ →
      (LinearMap.lTensor A ↑d) ⁅y_1, y⁆ = ⁅y_1, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) y_1⁆ →
        (LinearMap.lTensor A ↑d) ⁅x + y_1, y⁆ =
          ⁅x + y_1, (LinearMap.lTensor A ↑d) y⁆ - ⁅y, (LinearMap.lTensor A ↑d) (x + y_1)⁆
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:
by 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
⊢ { toFun := ⇑(LinearMap.lTensor A ↑(x✝¹ + x✝)), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } =
    { toFun := ⇑(LinearMap.lTensor A ↑x✝¹), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } +
      { toFun := ⇑(LinearMap.lTensor A ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }

Tactic:
ext _; 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
⊢ { toFun := ⇑(LinearMap.lTensor A ↑(x✝¹ • x✝)), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ } =
    (RingHom.id R) x✝¹ • { toFun := ⇑(LinearMap.lTensor A ↑x✝), map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }

Tactic:
ext _; 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:
by simp

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

Goal state before:
pp: case mk.mk.mk
R : Type u
X : Type v
inst✝ : CommRing R
x✝ : FreeLieAlgebra R X
a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y✝ : FreeLieAlgebra R X
b : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z✝ : FreeLieAlgebra R X
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.mk (Rel R X) ((a + b) * c) = Quot.mk (Rel R X) (a * c + b * c)

Tactic:
add_mul

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

Goal state before:
pp: R : Type u
X : Type v
inst✝ : CommRing R
⊢ ∀ (x : FreeLieAlgebra R X), Quot.map₂ (fun x1 x2 ↦ x1 * x2) ⋯ ⋯ x x = 0

Tactic:
rintro ⟨a⟩; exact Quot.sound (Rel.lie_self a)

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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by simp

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

Goal state before:
pp: case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : R[M]
m : M
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.coeff.support
ih :
  ∀ (hx : y ∈ gradeBy R (⇑f) (f m)),
    (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, hx⟩
hmby : single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.coeff.support ⊆ ⇑f ⁻¹' {f m}
ih' : (decomposeAux f) y = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, h2⟩ := ih h2
⊢ (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m b, ⋯⟩ + (decomposeAux f) y =
    (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m b + y, hmby⟩

Tactic:
ih',

Goal state after:
case refine_2
M : Type u_1
ι : Type u_2
R : Type u_3
inst✝³ : AddMonoid M
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
x : R[M]
m : M
b : R
y : R[M]
hmy : m ∉ y.coeff.support
hb : b ≠ 0
this : Disjoint (Finsupp.single m b).support y.coeff.support
ih :
  ∀ (hx : y ∈ gradeBy R (⇑f) (f m)),
    (decomposeAux f) ↑⟨y, hx⟩ = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, hx⟩
hmby : single m b + y ∈ gradeBy R (⇑f) (f m)
h1 : ↑(Finsupp.single m b).support ⊆ ⇑f ⁻¹' {f m}
h2 : ↑y.coeff.support ⊆ ⇑f ⁻¹' {f m}
ih' : (decomposeAux f) y = (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, h2⟩ := ih h2
⊢ (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m b, ⋯⟩ +
      (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨y, h2⟩ =
    (DirectSum.of (fun i ↦ ↥(gradeBy R (⇑f) i)) (f m)) ⟨single m b + y, hmby⟩
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:
by 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)
      (⁅((ofProd c).symm x).1, ((ofProd c).symm x).1⁆,
        (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm x).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm x).2⁆ -
          ⁅((ofProd c).symm x).1, ((ofProd c).symm x).2⁆) =
    0

Tactic:
rw [← of_zero, c.1.2]

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 : ofTwoCocycle c
⊢ (ofProd 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⁆) =
    (ofProd c) 0
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:
by 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:
by 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:
by 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 ⋊⁅ψ⁆ L
⊢ ⁅x✝, x✝⁆ = 0

Tactic:
by 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
⊢ { left := x✝¹ + x✝, right := 0 } = { left := x✝¹, right := 0 } + { left := x✝, right := 0 }

Tactic:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by simp

Goal state after: