mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
this✝ : Module.Finite K R
this : IsReduced R
⊢ (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯)
      ((aeval ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f})) p))
        (minpoly K ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f})) p))) =
    0

Tactic:
minpoly.aeval,

Goal state after:
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
p : K[X]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
this✝ : Module.Finite K R
this : IsReduced R
⊢ (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) 0 = 0
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: case succ
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
⊢ (⇑D)^[n + 1] ⁅a, b⁆ = ∑ ij ∈ antidiagonal (n + 1), (n + 1).choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆

Tactic:
rw [sum_antidiagonal_choose_succ_nsmul (M := L) (fun i j => ⁅D^[i] a, D^[j] b⁆) n]

Goal state after:
case succ
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
⊢ (⇑D)^[n + 1] ⁅a, b⁆ =
    ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2 + 1] b⁆ +
      ∑ ij ∈ antidiagonal n, n.choose ij.2 • ⁅(⇑D)^[ij.1 + 1] a, (⇑D)^[ij.2] b⁆
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 : M
⊢ ∀ (a b : L),
    ((↑(LieModule.toEnd R L M)).flip m) ⁅a, b⁆ =
      ⁅a, ((↑(LieModule.toEnd R L M)).flip m) b⁆ - ⁅b, ((↑(LieModule.toEnd R L M)).flip m) a⁆

Tactic:
by simp

Goal state after:
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 y : L
D : LieDerivation R L M
⊢ (inner R L M) (D (x + y)) = (inner R L M) (D x) + (inner R L M) (D y)

Tactic:
by simp

Goal state after:
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₁ D₂ : LieDerivation R L M
⊢ (inner R L M) ((D₁ + D₂) x) = (inner R L M) (D₁ x) + (inner R L M) (D₂ x)

Tactic:
by simp

Goal state after:
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 y : L
D : LieDerivation R L M
⊢ (inner R L M) (((inner R L M) (D y)) x) = (inner R L M) (D ⁅x, y⁆) + (inner R L M) (((inner R L M) (D x)) y)

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]},
      p.Monic →
        p.natDegree = m →
          ∃ S x x_1,
            ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
hp : Monic 1
hn : natDegree 1 = n
hpu : IsUnit 1
⊢ (Polynomial.map (algebraMap R R) 1).Splits

Tactic:
by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: case refine_4
M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝⁵ : Module.Finite K R
this✝⁴ : Module.Finite R S
this✝³ : Module.Finite K S
this✝² : IsArtinianRing R
this✝¹ : IsReduced R
this✝ : IsReduced S
φ : S →ₐ[K] End K M :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
this : K[f, g] ≤ φ.range
p : S
ha : φ p ∈ K[f, g]
⊢ φ ((aeval p) (minpoly K p)) = 0

Tactic:
minpoly.aeval,

Goal state after:
case refine_4
M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝⁵ : Module.Finite K R
this✝⁴ : Module.Finite R S
this✝³ : Module.Finite K S
this✝² : IsArtinianRing R
this✝¹ : IsReduced R
this✝ : IsReduced S
φ : S →ₐ[K] End K M :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
this : K[f, g] ≤ φ.range
p : S
ha : φ p ∈ K[f, g]
⊢ φ 0 = 0
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case e'_4
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  (aeval
        (P.newtonMap^[n] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P =
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
this : IsUnit ((aeval (P.newtonMap^[n] x)) (derivative P))
⊢ (aeval (P.newtonMap^[n] x)) P + -1 * (aeval (P.newtonMap^[n] x)) P = 0

Tactic:
neg_mul,

Goal state after:
case e'_4
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  (aeval
        (P.newtonMap^[n] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P =
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
this : IsUnit ((aeval (P.newtonMap^[n] x)) (derivative P))
⊢ (aeval (P.newtonMap^[n] x)) P + -(1 * (aeval (P.newtonMap^[n] x)) P) = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]},
      p.Monic →
        p.natDegree = m →
          ∃ S x x_1,
            ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq : Polynomial.map (algebraMap R (AdjoinRoot p)) p = (X - C (AdjoinRoot.root p)) * q
hqm : q.Monic
this✝¹ : Free R (AdjoinRoot p)
this✝ : Module.Finite R (AdjoinRoot p)
this : Nontrivial (AdjoinRoot p)
S : Type u
w✝⁴ : CommRing S
w✝³ : Algebra (AdjoinRoot p) S
w✝² : Module.Finite (AdjoinRoot p) S
w✝¹ : Free (AdjoinRoot p) S
w✝ : Nontrivial S
hS : (Polynomial.map (algebraMap (AdjoinRoot p) S) q).Splits
algInst✝ : Algebra R S := ((algebraMap (AdjoinRoot p) S).comp (algebraMap R (AdjoinRoot p))).toAlgebra
scalarTowerInst✝ : IsScalarTower R (AdjoinRoot p) S := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S))
⊢ (Polynomial.map (algebraMap (AdjoinRoot p) S) (X - C (AdjoinRoot.root p))).Splits

Tactic:
by simp

Goal state after:
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: case succ.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  (aeval
        (P.newtonMap^[n] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P =
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
⊢ (aeval x) P ^ 2 ^ (n + 1) ∣
    (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2

Tactic:
neg_mul,

Goal state after:
case succ.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsNilpotent ((aeval x) P)
h' : IsUnit ((aeval x) (derivative P))
n : ℕ
ih : (aeval x) P ^ 2 ^ n ∣ (aeval (P.newtonMap^[n] x)) P
d : S
hd :
  (aeval
        (P.newtonMap^[n] x +
          -Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P))
      P =
    (aeval (P.newtonMap^[n] x)) P +
        eval (P.newtonMap^[n] x) (derivative (map (algebraMap R S) P)) *
          (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) +
      d * (-Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P) ^ 2
⊢ (aeval x) P ^ 2 ^ (n + 1) ∣
    (-(Ring.inverse ((aeval (P.newtonMap^[n] x)) (derivative P)) * (aeval (P.newtonMap^[n] x)) P)) ^ 2
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
l k : ℕ
ih : D (k + l) I = D k (D l I)
⊢ D (k + 1 + l) I = D (k + 1) (D l I)

Tactic:
| succ k ih =>

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

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
k : ℕ
ih : ∀ {l : ℕ}, l ≤ k → D k I ≤ D l J
l : ℕ
h₂ : l ≤ k + 1
⊢ D (k + 1) I ≤ D l J

Tactic:
| succ k ih =>

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

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
I : LieIdeal R L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
k : ℕ
ih : derivedSeriesOfIdeal A (A ⊗[R] L) k (LieSubmodule.baseChange A I) = LieSubmodule.baseChange A (D k I)
⊢ derivedSeriesOfIdeal A (A ⊗[R] L) (k + 1) (LieSubmodule.baseChange A I) = LieSubmodule.baseChange A (D (k + 1) I)

Tactic:
| succ k ih =>

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

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
a : A
⊢ ∀ (y : L), ((bracket' R A L L) (a ⊗ₜ[R] y)) (a ⊗ₜ[R] y) = 0

Tactic:
l

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
a : A
l : L
⊢ ((bracket' R A L L) (a ⊗ₜ[R] l)) (a ⊗ₜ[R] l) = 0
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
ih : derivedSeries R (↥I) k = comap I.incl (derivedSeriesOfIdeal R L k I)
⊢ derivedSeries R (↥I) (k + 1) = comap I.incl (derivedSeriesOfIdeal R L (k + 1) I)

Tactic:
| succ k ih =>

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

Goal state before:
pp: case succ
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
k : ℕ
ih : map f (derivedSeries R L' k) ≤ derivedSeries R L k
⊢ map f (derivedSeries R L' (k + 1)) ≤ derivedSeries R L (k + 1)

Tactic:
| succ k ih =>

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

Goal state before:
pp: case succ
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
h : Function.Surjective ⇑f
k : ℕ
ih : map f (derivedSeries R L' k) = derivedSeries R L k
⊢ map f (derivedSeries R L' (k + 1)) = derivedSeries R L (k + 1)

Tactic:
| succ k ih =>

Goal state after:
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 N₁ N₂ : LieSubmodule R L M
x : L
⊢ ⁅x, 0⁆ ∈ N

Tactic:
by simp

Goal state after:
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 N₁ N₂ : LieSubmodule R L M
⊢ 0 ∈ {x | ∀ (m : M), ⁅x, m⁆ ∈ N}

Tactic:
by simp

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

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ↑↑(derivedSeriesOfIdeal R L k ⊤) = ↑↑(derivedSeriesOfIdeal ℤ L k ⊤)
⊢ ↑↑(derivedSeriesOfIdeal R L (k + 1) ⊤) = ↑↑(derivedSeriesOfIdeal ℤ L (k + 1) ⊤)

Tactic:
| succ k ih =>

Goal state after:
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
N₁ N₂ : LieSubmodule R L M
k : ℕ
ih : lcs k (N₁ ⊔ N₂) = lcs k N₁ ⊔ lcs k N₂
⊢ lcs (k + 1) (N₁ ⊔ N₂) = lcs (k + 1) N₁ ⊔ lcs (k + 1) N₂

Tactic:
| succ k ih =>

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'
f : L' →ₗ⁅R⁆ L
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
k : ℕ
hk : derivedSeries R L' k = ⊥
⊢ derivedSeries R L k = ⊥

Tactic:
rw [← LieIdeal.derivedSeries_map_eq k h, hk]

Goal state after:
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' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
k : ℕ
hk : derivedSeries R L' k = ⊥
⊢ LieIdeal.map f ⊥ = ⊥
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✝¹⁶ : 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
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y : A ⊗[R] L
⊢ (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) 0) y) =
    ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) 0))
      ((TensorProduct.map f.toLinearMap ↑g) y)

Tactic:
by simp

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✝¹⁶ : 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
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y : A ⊗[R] L
⊢ (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) x) y) =
    ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) x))
      ((TensorProduct.map f.toLinearMap ↑g) y)

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

Goal state after:
case 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
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y : A ⊗[R] L
⊢ ∀ (x : A) (y_1 : L),
    (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x ⊗ₜ[R] y_1)) y) =
      ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x ⊗ₜ[R] y_1)))
        ((TensorProduct.map f.toLinearMap ↑g) y)

case 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
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y : A ⊗[R] L
⊢ ∀ (x y_1 : A ⊗[R] L),
    (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) x) y) =
        ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) x))
          ((TensorProduct.map f.toLinearMap ↑g) y) →
      (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) y_1) y) =
          ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) y_1))
            ((TensorProduct.map f.toLinearMap ↑g) y) →
        (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x + y_1)) y) =
          ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x + y_1)))
            ((TensorProduct.map f.toLinearMap ↑g) y)
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✝¹⁶ : 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
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y : A ⊗[R] L
x✝ : A
y✝ : L
⊢ (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x✝ ⊗ₜ[R] y✝)) 0) =
    ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x✝ ⊗ₜ[R] y✝)))
      ((TensorProduct.map f.toLinearMap ↑g) 0)

Tactic:
by simp

Goal state after:
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
k : ℕ
ih : ↑↑(lowerCentralSeries R L M k) = ↑↑(lowerCentralSeries ℤ L M k)
⊢ ↑↑(lowerCentralSeries R L M (k + 1)) = ↑↑(lowerCentralSeries ℤ L M (k + 1))

Tactic:
| succ k ih =>

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✝¹⁶ : 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
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y : A ⊗[R] L
x✝² : A
y✝ : L
x✝¹ : A
x✝ : L
⊢ (TensorProduct.map f.toLinearMap ↑g) (((LieAlgebra.ExtendScalars.bracket'✝ R A L L) (x✝² ⊗ₜ[R] y✝)) (x✝¹ ⊗ₜ[R] x✝)) =
    ((LieAlgebra.ExtendScalars.bracket'✝ R B L' L') ((TensorProduct.map f.toLinearMap ↑g) (x✝² ⊗ₜ[R] y✝)))
      ((TensorProduct.map f.toLinearMap ↑g) (x✝¹ ⊗ₜ[R] x✝))

Tactic:
by simp

Goal state after:
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
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lcs k N ≤ N
⊢ lcs (k + 1) N ≤ N

Tactic:
| succ k ih =>

Goal state after:
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
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : lowerCentralSeries R L (↥N) k = comap N.incl (lcs k N)
⊢ lowerCentralSeries R L (↥N) (k + 1) = comap N.incl (lcs (k + 1) N)

Tactic:
| succ k ih =>

Goal state after: