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

Goal state before:
pp: case succ.a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R L k ⊤ ↔ x ∈ derivedSeriesOfIdeal ℤ L k ⊤
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x}) ⊆
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})

pp: case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R L k ⊤ ↔ x ∈ derivedSeriesOfIdeal ℤ L k ⊤
⊢ ↑(Submodule.span ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x}) ⊆
    ↑(Submodule.span R {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})

Tactic:
·

Goal state after:
case succ.a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R L k ⊤ ↔ x ∈ derivedSeriesOfIdeal ℤ L k ⊤
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x}) ⊆
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) 0) z) =
    ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) 0)) z +
      ((bracket' R A L M) 0) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)

pp: case refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ ∀ (x : A) (y : L),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (x ⊗ₜ[R] y)) z) =
      ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y))) z +
        ((bracket' R A L M) (x ⊗ₜ[R] y)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)

pp: case refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) x) z) =
        ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) x)) z +
          ((bracket' R A L M) x) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z) →
      ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y)) z +
            ((bracket' R A L M) y) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z) →
        ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (x + y)) z) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x + y))) z +
            ((bracket' R A L M) (x + y)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)

Tactic:
·

Goal state after:
case refine_2.refine_1
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) 0) z) =
    ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) 0)) z +
      ((bracket' R A L M) 0) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R L k ⊤ ↔ x ∈ derivedSeriesOfIdeal ℤ L k ⊤
⊢ ↑(Submodule.span ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x}) ⊆
    ↑(Submodule.span R {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})

Tactic:
·

Goal state after:
case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R L k ⊤ ↔ x ∈ derivedSeriesOfIdeal ℤ L k ⊤
⊢ ↑(Submodule.span ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x}) ⊆
    ↑(Submodule.span R {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ ∀ (x : A) (y : L),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (x ⊗ₜ[R] y)) z) =
      ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y))) z +
        ((bracket' R A L M) (x ⊗ₜ[R] y)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)

pp: case refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) x) z) =
        ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) x)) z +
          ((bracket' R A L M) x) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z) →
      ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y)) z +
            ((bracket' R A L M) y) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z) →
        ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (x + y)) z) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x + y))) z +
            ((bracket' R A L M) (x + y)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)

Tactic:
·

Goal state after:
case refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ ∀ (x : A) (y : L),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (x ⊗ₜ[R] y)) z) =
      ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y))) z +
        ((bracket' R A L M) (x ⊗ₜ[R] y)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
⊢ H.normalizer ≤ H

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
⊢ H.normalizer ≤ H
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_2.refine_1
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) 0) =
    ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) 0 +
      ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) 0)

pp: case refine_2.refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ∀ (x : A) (y : M),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (x ⊗ₜ[R] y)) =
      ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) (x ⊗ₜ[R] y) +
        ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y))

pp: case refine_2.refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ∀ (x y : A ⊗[R] M),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) x) =
        ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) x +
          ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) x) →
      ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) y) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) y +
            ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) y) →
        ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (x + y)) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) (x + y) +
            ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (x + y))

Tactic:
·

Goal state after:
case refine_2.refine_2.refine_1
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) 0) =
    ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) 0 +
      ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) 0)
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ∀ (x : A) (y : M),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (x ⊗ₜ[R] y)) =
      ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) (x ⊗ₜ[R] y) +
        ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y))

pp: case refine_2.refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ∀ (x y : A ⊗[R] M),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) x) =
        ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) x +
          ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) x) →
      ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) y) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) y +
            ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) y) →
        ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (x + y)) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) (x + y) +
            ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (x + y))

Tactic:
·

Goal state after:
case refine_2.refine_2.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ∀ (x : A) (y : M),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (x ⊗ₜ[R] y)) =
      ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) (x ⊗ₜ[R] y) +
        ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (x ⊗ₜ[R] y))
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ∀ (x y : A ⊗[R] M),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) x) =
        ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) x +
          ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) x) →
      ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) y) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) y +
            ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) y) →
        ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (x + y)) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) (x + y) +
            ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (x + y))

Tactic:
·

Goal state after:
case refine_2.refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
a₂ : A
l₂ : L
⊢ ∀ (x y : A ⊗[R] M),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) x) =
        ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) x +
          ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) x) →
      ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) y) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) y +
            ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) y) →
        ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (x + y)) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂))) (x + y) +
            ((bracket' R A L M) (a₂ ⊗ₜ[R] l₂)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (x + y))
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) x) z) =
        ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) x)) z +
          ((bracket' R A L M) x) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z) →
      ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y)) z +
            ((bracket' R A L M) y) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z) →
        ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (x + y)) z) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x + y))) z +
            ((bracket' R A L M) (x + y)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)

Tactic:
·

Goal state after:
case refine_2.refine_3
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) x) z) =
        ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) x)) z +
          ((bracket' R A L M) x) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z) →
      ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) y)) z +
            ((bracket' R A L M) y) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z) →
        ((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) (((bracket' R A L M) (x + y)) z) =
          ((bracket' R A L M) (((bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) (x + y))) z +
            ((bracket' R A L M) (x + y)) (((bracket' R A L M) (a₁ ⊗ₜ[R] l₁)) z)
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case mp
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable L'
⊢ IsSolvable L

pp: case mpr
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable L
⊢ IsSolvable L'

Tactic:
·

Goal state after:
case mp
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable L'
⊢ IsSolvable L
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case mpr
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable L
⊢ IsSolvable L'

Tactic:
·

Goal state after:
case mpr
R : Type u
L : Type v
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable L
⊢ IsSolvable L'
Module: Mathlib.Algebra.Lie.Nilpotent

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
k : ℕ
⊢ ↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries ℤ L M k)

Tactic:
rw [← LieSubmodule.coe_toSubmodule, ← LieSubmodule.coe_toSubmodule]

Goal state after:
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
k : ℕ
⊢ ↑↑(lowerCentralSeries R L M k) = ↑↑(lowerCentralSeries ℤ L M k)
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_3
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
⊢ ∀ (x y_1 : A ⊗[R] L),
    ((bracket' R A L M) x) (((bracket' R A L M) y) z) =
        ((bracket' R A L M) (((bracket' R A L L) x) y)) z + ((bracket' R A L M) y) (((bracket' R A L M) x) z) →
      ((bracket' R A L M) y_1) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) y_1) y)) z + ((bracket' R A L M) y) (((bracket' R A L M) y_1) z) →
        ((bracket' R A L M) (x + y_1)) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) (x + y_1)) y)) z +
            ((bracket' R A L M) y) (((bracket' R A L M) (x + y_1)) z)

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
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 : A ⊗[R] L
z : A ⊗[R] M
⊢ ∀ (x y_1 : A ⊗[R] L),
    ((bracket' R A L M) x) (((bracket' R A L M) y) z) =
        ((bracket' R A L M) (((bracket' R A L L) x) y)) z + ((bracket' R A L M) y) (((bracket' R A L M) x) z) →
      ((bracket' R A L M) y_1) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) y_1) y)) z + ((bracket' R A L M) y) (((bracket' R A L M) y_1) z) →
        ((bracket' R A L M) (x + y_1)) (((bracket' R A L M) y) z) =
          ((bracket' R A L M) (((bracket' R A L L) (x + y_1)) y)) z +
            ((bracket' R A L M) y) (((bracket' R A L M) (x + y_1)) z)
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case refine_1
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L L)
⊢ ⊥ ∈ {I | IsSolvable ↥I}

pp: case refine_2
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L L)
I : LieSubmodule R L L
hI : I ∈ {I | IsSolvable ↥I}
J : LieSubmodule R L L
hJ : J ∈ {I | IsSolvable ↥I}
⊢ I ⊔ J ∈ {I | IsSolvable ↥I}

Tactic:
·

Goal state after:
case refine_1
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L L)
⊢ ⊥ ∈ {I | IsSolvable ↥I}
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case refine_2
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L L)
I : LieSubmodule R L L
hI : I ∈ {I | IsSolvable ↥I}
J : LieSubmodule R L L
hJ : J ∈ {I | IsSolvable ↥I}
⊢ I ⊔ J ∈ {I | IsSolvable ↥I}

Tactic:
·

Goal state after:
case refine_2
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L L)
I : LieSubmodule R L L
hI : I ∈ {I | IsSolvable ↥I}
J : LieSubmodule R L L
hJ : J ∈ {I | IsSolvable ↥I}
⊢ I ⊔ J ∈ {I | IsSolvable ↥I}