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

Goal state before:
pp: case refine_2
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ (Algebra.TensorProduct.lift (algHom T T (AdjoinRoot q)) (mapAlgHom includeRight p q ⋯) ⋯).comp
      (liftAlgHom q (Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))
        (1 ⊗ₜ[R] root p) ⋯) =
    AlgHom.id T (AdjoinRoot q)

Tactic:
ext

Goal state after:
case refine_2.hAlg
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
x✝ : S
⊢ ((AlgHom.restrictScalars R
            (((Algebra.TensorProduct.lift (algHom T T (AdjoinRoot q)) (mapAlgHom includeRight p q ⋯) ⋯).comp
                  (liftAlgHom q
                    (Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))
                    (1 ⊗ₜ[R] root p) ⋯)).comp
              (ofAlgHom T q))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R ((AlgHom.id T (AdjoinRoot q)).comp (ofAlgHom T q))).comp includeRight) x✝

case refine_2.hRoot
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ ((Algebra.TensorProduct.lift (algHom T T (AdjoinRoot q)) (mapAlgHom includeRight p q ⋯) ⋯).comp
        (liftAlgHom q (Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))
          (1 ⊗ₜ[R] root p) ⋯))
      (root q) =
    (AlgHom.id T (AdjoinRoot q)) (root q)
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
m n : M
⊢ (let __spread.0 := (↑(LieModule.toEnd R L M)).flip (m + n);
    { toLinearMap := __spread.0, leibniz' := ⋯ }) =
    (let __spread.0 := (↑(LieModule.toEnd R L M)).flip m;
      { toLinearMap := __spread.0, leibniz' := ⋯ }) +
      let __spread.0 := (↑(LieModule.toEnd R L M)).flip n;
      { toLinearMap := __spread.0, leibniz' := ⋯ }

Tactic:
ext

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
m n : M
a✝ : L
⊢ (let __spread.0 := (↑(LieModule.toEnd R L M)).flip (m + n);
      { toLinearMap := __spread.0, leibniz' := ⋯ })
      a✝ =
    ((let __spread.0 := (↑(LieModule.toEnd R L M)).flip m;
        { toLinearMap := __spread.0, leibniz' := ⋯ }) +
        let __spread.0 := (↑(LieModule.toEnd R L M)).flip n;
        { toLinearMap := __spread.0, leibniz' := ⋯ })
      a✝
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
t : R
m : M
⊢ (let __spread.0 := (↑(LieModule.toEnd R L M)).flip (t • m);
    { toLinearMap := __spread.0, leibniz' := ⋯ }) =
    (RingHom.id R) t •
      let __spread.0 := (↑(LieModule.toEnd R L M)).flip m;
      { toLinearMap := __spread.0, leibniz' := ⋯ }

Tactic:
ext

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
t : R
m : M
a✝ : L
⊢ (let __spread.0 := (↑(LieModule.toEnd R L M)).flip (t • m);
      { toLinearMap := __spread.0, leibniz' := ⋯ })
      a✝ =
    ((RingHom.id R) t •
        let __spread.0 := (↑(LieModule.toEnd R L M)).flip m;
        { toLinearMap := __spread.0, leibniz' := ⋯ })
      a✝
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x : L
D : LieDerivation R L M
⊢ ⁅x, ↑D⁆ = ↑⁅x, D⁆

Tactic:
ext

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x : L
D : LieDerivation R L M
x✝ : L
⊢ ⁅x, ↑D⁆ x✝ = ↑⁅x, D⁆ x✝
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
t : R
x : L
D : LieDerivation R L M
⊢ ⁅t • x, D⁆ = t • ⁅x, D⁆

Tactic:
ext

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
t : R
x : L
D : LieDerivation R L M
a✝ : L
⊢ ⁅t • x, D⁆ a✝ = (t • ⁅x, D⁆) a✝
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
t : R
x : L
D : LieDerivation R L M
⊢ ⁅x, t • D⁆ = t • ⁅x, D⁆

Tactic:
ext

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
t : R
x : L
D : LieDerivation R L M
a✝ : L
⊢ ⁅x, t • D⁆ a✝ = (t • ⁅x, D⁆) a✝
Module: Mathlib.Algebra.Lie.AdjointAction.Derivation

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ ↑((ad R L) x) = (LieAlgebra.ad R L) x

Tactic:
ext

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x x✝ : L
⊢ ↑((ad R L) x) x✝ = ((LieAlgebra.ad R L) x) x✝
Module: Mathlib.Algebra.Lie.AdjointAction.Derivation

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
⊢ ⁅(ad R L) x, D⁆ = ⁅x, D⁆

Tactic:
ext

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D : LieDerivation R L L
a✝ : L
⊢ ⁅(ad R L) x, D⁆ a✝ = ⁅x, D⁆ a✝
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : LinearOrder R
x y : R
⊢ Associated |x| y ↔ Associated x y

Tactic:
obtain h | h := abs_choice x <;>
  simp [h]

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

Goal state before:
pp: case refine_3
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
inst✝¹⁷ : LieRing L
inst✝¹⁶ : LieAlgebra R L
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : LieRingModule L M
inst✝¹² : LieModule R L M
inst✝¹¹ : AddCommGroup N
inst✝¹⁰ : Module R N
inst✝⁹ : LieRingModule L N
inst✝⁸ : LieModule R L N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
f : M →ₗ⁅R,L⁆ P
g : N →ₗ⁅R,L⁆ Q
x : L
t : M ⊗[R] N
⊢ ∀ (x_1 y : M ⊗[R] N),
    (TensorProduct.map ↑f ↑g) ⁅x, x_1⁆ = ⁅x, (TensorProduct.map ↑f ↑g) x_1⁆ →
      (TensorProduct.map ↑f ↑g) ⁅x, y⁆ = ⁅x, (TensorProduct.map ↑f ↑g) y⁆ →
        (TensorProduct.map ↑f ↑g) ⁅x, x_1 + y⁆ = ⁅x, (TensorProduct.map ↑f ↑g) (x_1 + y)⁆

Tactic:
· intro t₁ t₂ ht₁ ht₂; simp only [ht₁, ht₂, lie_add, map_add]

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
⊢ (∃ x n, ⁅↑x, ↑n⁆ = m) ↔ ∃ a ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}, ↑(toModuleHom R L M) a = m

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
⊢ (∃ x n, ⁅↑x, ↑n⁆ = m) → ∃ a ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}, ↑(toModuleHom R L M) a = m

case mpr
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
⊢ (∃ a ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}, ↑(toModuleHom R L M) a = m) → ∃ x n, ⁅↑x, ↑n⁆ = m
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: case h
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ x ⊗ₜ[R] n ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t} ∧ ↑(toModuleHom R L M) (x ⊗ₜ[R] n) = ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆

Tactic:
constructor

Goal state after:
case h.left
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ x ⊗ₜ[R] n ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}

case h.right
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ↑(toModuleHom R L M) (x ⊗ₜ[R] n) = ⁅↑⟨x, hx⟩, ↑⟨n, hn⟩⁆
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: R : Type u_4
B : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : NonUnitalNonAssocRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : Module ℚ B
D : B →ₗ[R] B
h_der : ∀ (x y : B), D (x * y) = x * D y + D x * y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
⊢ Commute DL DR

Tactic:
ext

Goal state after:
R : Type u_4
B : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : NonUnitalNonAssocRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : Module ℚ B
D : B →ₗ[R] B
h_der : ∀ (x y : B), D (x * y) = x * D y + D x * y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
x✝¹ x✝ : B
⊢ ((AlgebraTensorModule.curry (DL * DR)) x✝¹) x✝ = ((AlgebraTensorModule.curry (DR * DL)) x✝¹) x✝
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: R : Type u_4
B : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : NonUnitalNonAssocRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : Module ℚ B
D : B →ₗ[R] B
h_der : ∀ (x y : B), D (x * y) = x * D y + D x * y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := ⋯
DR : End R (B ⊗[R] B) := ⋯
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := ⋯
hm : m = LinearMap.mul' R B
⊢ D ∘ₗ m = m ∘ₗ (DL + DR)

Tactic:
ext

Goal state after:
R : Type u_4
B : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : NonUnitalNonAssocRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : Module ℚ B
D : B →ₗ[R] B
h_der : ∀ (x y : B), D (x * y) = x * D y + D x * y
h_nil : IsNilpotent D
x y : B
DL : End R (B ⊗[R] B) := LinearMap.lTensor B D
DR : End R (B ⊗[R] B) := LinearMap.rTensor B D
h_nilL : IsNilpotent DL
h_nilR : IsNilpotent DR
h_comm : Commute DL DR
m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B
hm : m = LinearMap.mul' R B
x✝¹ x✝ : B
⊢ ((AlgebraTensorModule.curry (D ∘ₗ m)) x✝¹) x✝ = ((AlgebraTensorModule.curry (m ∘ₗ (DL + DR))) x✝¹) x✝
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N₁ N₂ : LieSubmodule R L M
⊢ (N₁ ⊓ N₂).normalizer = N₁.normalizer ⊓ N₂.normalizer

Tactic:
ext

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N₁ N₂ : LieSubmodule R L M
m✝ : M
⊢ m✝ ∈ (N₁ ⊓ N₂).normalizer ↔ m✝ ∈ N₁.normalizer ⊓ N₂.normalizer
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
M : 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
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N : LieSubmodule R L M
f : M' →ₗ⁅R,L⁆ M
⊢ comap f N.normalizer = (comap f N).normalizer

Tactic:
ext

Goal state after:
R : Type u_1
L : Type u_2
M : 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
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N : LieSubmodule R L M
f : M' →ₗ⁅R,L⁆ M
m✝ : M'
⊢ m✝ ∈ comap f N.normalizer ↔ m✝ ∈ (comap f N).normalizer
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
⊢ ⁅⊤, N⁆ ≤ N' ↔ N ≤ N'.normalizer

Tactic:
rw [lie_le_iff]

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
⊢ (∀ x ∈ ⊤, ∀ m ∈ N, ⁅x, m⁆ ∈ N') ↔ N ≤ N'.normalizer
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: 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'
f : L' →ₗ⁅R⁆ L
hL : IsSolvable L
h : Injective ⇑f
⊢ IsSolvable L'

Tactic:
by
  rw [isSolvable_iff R] at hL ⊢
  apply hL.imp
  intro k hk
  apply LieIdeal.bot_of_map_eq_bot h; rw [eq_bot_iff, ← hk]
  apply LieIdeal.derivedSeries_map_le

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

Goal state before:
pp: 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
⊢ IsSolvable L' ↔ IsSolvable L

Tactic:
constructor

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
⊢ IsSolvable L' → IsSolvable L

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
⊢ 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:
← 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: R : Type u_1
A : 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
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : L
⊢ (toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x) = LinearMap.baseChange A ((toEnd R L M) x)

Tactic:
ext

Goal state after:
R : Type u_1
A : 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
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : L
x✝ : M
⊢ ((TensorProduct.AlgebraTensorModule.curry ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x))) 1) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (LinearMap.baseChange A ((toEnd R L M) x))) 1) x✝
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
⊢ IsTrivial L M ↔ lowerCentralSeries R L M 1 = ⊥

Tactic:
constructor

Goal state after:
case mp
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
⊢ IsTrivial L M → lowerCentralSeries R L M 1 = ⊥

case mpr
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
⊢ lowerCentralSeries R L M 1 = ⊥ → IsTrivial L M
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
m : M
k : ℕ
ih : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)
hk : 2 * k.succ = 2 * k + 1 + 1
⊢ (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k + 1] m ∈ lowerCentralSeries R L M (2 * (k + 1))

Tactic:
simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ', hk,
      toEnd_apply_apply, LinearMap.coe_comp, toEnd_apply_apply]

Goal state after:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
m : M
k : ℕ
ih : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)
hk : 2 * k.succ = 2 * k + 1 + 1
⊢ ⁅x, ⁅y, (⇑((toEnd R L M) x) ∘ ⇑((toEnd R L M) y))^[k] m⁆⁆ ∈ ⁅⊤, ⁅⊤, lowerCentralSeries R L M (2 * k)⁆⁆
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
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
k : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
⊢ LieSubmodule.map f (lowerCentralSeries R L M 0) ≤ lowerCentralSeries R L M₂ 0

Tactic:
simp only [lowerCentralSeries_zero, le_top]

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

Goal state before:
pp: R : Type u_1
A : 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
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
⊢ ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s

Tactic:
ext

Goal state after:
R : Type u_1
A : 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
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
x✝ : A ⊗[R] M
⊢ x✝ ∈ ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} ↔ x✝ ∈ s
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
⊢ (mk' N).ker = N

Tactic:
ext

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
m✝ : M
⊢ m✝ ∈ (mk' N).ker ↔ m✝ ∈ N
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
⊢ HSMul.hSMul m = map (MulSemiringAction.toRingHom M R m)

Tactic:
ext

Goal state after:
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
x✝ : R[X]
n✝ : ℕ
⊢ (m • x✝).coeff n✝ = (map (MulSemiringAction.toRingHom M R m) x✝).coeff n✝
Module: Mathlib.FieldTheory.Finiteness

Goal state before:
pp: K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ IsNoetherian K V ↔ (Basis.ofVectorSpaceIndex K V).Finite

Tactic:
constructor

Goal state after:
case mp
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := ⋯
⊢ IsNoetherian K V → (Basis.ofVectorSpaceIndex K V).Finite

case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := ⋯
⊢ (Basis.ofVectorSpaceIndex K V).Finite → IsNoetherian K V
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 (↥(toEnd R L M).range) M k = ⊥) ↔ ∃ k, lowerCentralSeries R L M k = ⊥

Tactic:
constructor

Goal state after:
case mp
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 (↥(toEnd R L M).range) M k = ⊥) → ∃ k, lowerCentralSeries R L M k = ⊥

case mpr
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 = ⊥) → ∃ k, lowerCentralSeries R (↥(toEnd R L M).range) M k = ⊥