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

Goal state before:
pp: case refine_2
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 : M) (y : N), (TensorProduct.map ↑f ↑g) ⁅x, x_1 ⊗ₜ[R] y⁆ = ⁅x, (TensorProduct.map ↑f ↑g) (x_1 ⊗ₜ[R] y)⁆

Tactic:
intro m n
        simp only [LieModuleHom.coe_toLinearMap, lie_tmul_right, LieModuleHom.map_lie, map_tmul,
          map_add]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
ha : IsNilpotent a
⊢ IsNilpotent (exp a - 1)

Tactic:
by
  nontriviality A
  rw [exp, ← Nat.sub_add_cancel (pos_nilpotencyClass_iff.2 ha), Finset.sum_range_succ']
  simp only [Nat.succ_eq_add_one, zero_add, Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero,
    one_smul, add_sub_cancel_right]
  apply Commute.isNilpotent_sum fun _ _ ↦ smul (pow_of_pos ha <| by positivity) _
  simp [Nat.factorial_ne_zero]

Goal state after:
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
h_comm : Commute DL DR
⊢ (exp D) (x * y) = (exp D) x * (exp D) y

Tactic:
set m : B ⊗[R] B →ₗ[R] B := LinearMap.mul' R B with hm

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
⊢ (exp D) (x * y) = (exp D) x * (exp D) y
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 : Injective ⇑f
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ derivedSeries R L' k = ⊥

Tactic:
apply LieIdeal.bot_of_map_eq_bot h

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 : Injective ⇑f
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ LieIdeal.map f (derivedSeries R L' 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✝⁷ : 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
⊢ ∀ (t : R) (x y : A ⊗[R] L), ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
simp [bracket_def]

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:
simp only [lcs_succ, lowerCentralSeries_succ] at ih ⊢
    have : N.lcs k ≤ N.incl.range := by
      rw [N.range_incl]
      apply lcs_le_self
    rw [ih, LieSubmodule.comap_bracket_eq _ N.incl _ N.ker_incl this]

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

Goal state before:
pp: R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
n i j : ℕ
hxn : (toEnd R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ I.lcs M j
l : ℕ
⊢ ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))

Tactic:
induction l with

Goal state after:
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
x✝ : eval (m • x) (m • (C r * X ^ n)) = m • eval x (C r * X ^ n)
⊢ eval (m • x) (C (m • r) * X ^ (n + 1)) = m • eval x (C r * X ^ (n + 1))

Tactic:
eval_mul,

Goal state after:
M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
x✝ : eval (m • x) (m • (C r * X ^ n)) = m • eval x (C r * X ^ n)
⊢ eval (m • x) (C (m • r)) * eval (m • x) (X ^ (n + 1)) = m • eval x (C r * X ^ (n + 1))
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
l : ℕ
⊢ lowerCentralSeries R L M (l * n) ≤ I.lcs M l

Tactic:
induction l with

Goal state after:
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
x✝ : eval (m • x) (m • (C r * X ^ n)) = m • eval x (C r * X ^ n)
⊢ m • r * (m • x) ^ (n + 1) = m • eval x (C r * X ^ (n + 1))

Tactic:
eval_mul,

Goal state after:
M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
x✝ : eval (m • x) (m • (C r * X ^ n)) = m • eval x (C r * X ^ n)
⊢ m • r * (m • x) ^ (n + 1) = m • (eval x (C r) * eval x (X ^ (n + 1)))
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
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ ucs k N = ⊤ ↔ LieModule.lowerCentralSeries R L M k ≤ N

Tactic:
rw [eq_top_iff, ← lcs_le_iff]; rfl

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Algebraic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
⊢ finrank (↥E) L ∣ finrank (↥F) L

Tactic:
by
  let _ := (inclusion h).toRingHom.toAlgebra
  have : IsScalarTower F E L := IsScalarTower.of_algebraMap_eq fun x ↦ rfl
  exact Module.finrank_dvd_finrank_left F E L

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ ∑ x ∈ s, g • l x * (toFun G F) x g' - ∑ x ∈ s, l x • (toFun G F) x g' = 0 g'

Tactic:
Pi.zero_apply,

Goal state after:
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ ∑ x ∈ s, g • l x * (toFun G F) x g' - ∑ x ∈ s, l x • (toFun G F) x g' = 0
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
hS : ∀ x ∈ S, IsAlgebraic F x
⊢ adjoin F S = ⊤ ↔ Algebra.adjoin F S = ⊤

Tactic:
by
  rw [← IntermediateField.adjoin_toSubalgebra_of_isAlgebraic hS,
      ← IntermediateField.toSubalgebra_inj,
      IntermediateField.top_toSubalgebra]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : CommRing M
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R M
inst✝⁴ : Algebra K M
inst✝³ : IsScalarTower R K M
x : M
inst✝² : Algebra K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
int : IsIntegral R x
h : (Polynomial.map ((algebraMap K L).comp (algebraMap R K)) (minpoly R x)).Splits
⊢ (Polynomial.map (algebraMap K L) (minpoly K x)).Splits

Tactic:
exact int.minpoly_splits_tower_top' h

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : Lifts F E K
x : ↥{ carrier := ⊥, emb := (Algebra.ofId F K).comp ↑(botEquiv F E) }.carrier
⊢ L.emb ((inclusion ⋯) x) = { carrier := ⊥, emb := (Algebra.ofId F K).comp ↑(botEquiv F E) }.emb x

Tactic:
obtain ⟨x, rfl⟩ := (botEquiv F E).symm.surjective x

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : Lifts F E K
x : F
⊢ L.emb ((inclusion ⋯) ((botEquiv F E).symm x)) =
    { carrier := ⊥, emb := (Algebra.ofId F K).comp ↑(botEquiv F E) }.emb ((botEquiv F E).symm x)
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L₁ L₂ : Lifts F E K
c : Set (Lifts F E K)
hc✝ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
t : ↑(insert ⊥ c) → IntermediateField F E := fun i ↦ (↑i).carrier
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) t
i j : ↑(insert ⊥ c)
h : (t i).toSubalgebra ≤ (t j).toSubalgebra
x : ↥(↑i).carrier
hji : ↑j ≤ ↑i
⊢ (↑i).emb x = (↑i).emb ((AlgHom.id F ↥(t i)) x)

Tactic:
AlgHom.id_apply x

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L₁ L₂ : Lifts F E K
c : Set (Lifts F E K)
hc✝ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
t : ↑(insert ⊥ c) → IntermediateField F E := fun i ↦ (↑i).carrier
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) t
i j : ↑(insert ⊥ c)
h : (t i).toSubalgebra ≤ (t j).toSubalgebra
x : ↥(↑i).carrier
hji : ↑j ≤ ↑i
⊢ (↑i).emb x = (↑i).emb x
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case refine_1
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)
x : E
hx : x ∈ ⨆ i, f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ adjoin F ((minpoly F x1).rootSet E) ≤ adjoin F ((minpoly F ⟨i, ⟨x1, hx1⟩⟩.snd).rootSet E)

pp: case refine_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)
x : E
hx : x ∈ ⨆ i, f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ x1 ∈ (minpoly F x1).rootSet E

Tactic:
· rw [IntermediateField.minpoly_eq, Subtype.coe_mk]

Goal state after:
case refine_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)
x : E
hx : x ∈ ⨆ i, f i
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ x1 ∈ (minpoly F x1).rootSet E
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo ⇑(f i) ↑p ↑p
h✝ : Nonempty ι
⊢ p ⊓ ⨅ i, (f i).maxGenEigenspace (μ i) =
    Submodule.map p.subtype (⨅ i, maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))

Tactic:
simp_rw [inf_iInf, p.inf_genEigenspace _ (hfp _), Submodule.map_iInf _ p.injective_subtype]

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case refine_1
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
L : IntermediateField F E
f : ↥L →ₐ[F] K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this✝¹ : Algebra ↥{ carrier := L, emb := f }.carrier ↥φ.carrier := (inclusion ⋯).toAlgebra
this✝ : SMul ↥L ↥φ.carrier := this✝¹.toSMul
this : IsScalarTower (↥L) (↥φ.carrier) E
⊢ (Polynomial.map (φ.emb.comp (algebraMap ↥L ↥φ.carrier)) (minpoly (↥L) s)).Splits

Tactic:
convert! (hK s h).2; ext; apply hfφ.2

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
x : E
y : K
hx : x ∈ adjoin F S
hy : (aeval y) (minpoly F x) = 0
⊢ ∃ φ, φ ⟨x, hx⟩ = y

Tactic:
by
  have := isAlgebraic_adjoin (fun s hs ↦ (hK s hs).1)
  have ix : IsAlgebraic F _ := Algebra.IsAlgebraic.isAlgebraic (⟨x, hx⟩ : adjoin F S)
  rw [isAlgebraic_iff_isIntegral, isIntegral_iff] at ix
  obtain ⟨φ, hφ⟩ := exists_algHom_adjoin_of_splits hK ((algHomAdjoinIntegralEquiv F ix).symm
    ⟨y, mem_aroots.mpr ⟨minpoly.ne_zero ix, hy⟩⟩) (adjoin_simple_le_iff.mpr hx)
  exact ⟨φ, (DFunLike.congr_fun hφ <| AdjoinSimple.gen F x).trans <|
    algHomAdjoinIntegralEquiv_symm_apply_gen F ix _⟩

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : 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✝¹ : LieRing.IsNilpotent L
inst✝ : IsNoetherian R M
x : L
⊢ _root_.IsNilpotent ((toEnd R L ↥(genWeightSpace M 0)) x)

Tactic:
by
  simpa using isNilpotent_toEnd_sub_algebraMap M (0 : L → R) x

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : 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✝ : LieRing.IsNilpotent L
x : L
k : ℕ
m : M
l : ℕ
⊢ ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l

Tactic:
induction l with

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : 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✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
y : L
m : M
hm : ∀ (k : ℕ), ∃ n, ((toEnd R L M) y ^ k) n = m
k : ℕ
⊢ ∃ n, ((toEnd R L M₂) y ^ k) n = f m

Tactic:
obtain ⟨n, hn⟩ := hm k

Goal state after:
R : 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✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
y : L
m : M
hm : ∀ (k : ℕ), ∃ n, ((toEnd R L M) y ^ k) n = m
k : ℕ
n : M
hn : ((toEnd R L M) y ^ k) n = m
⊢ ∃ n, ((toEnd R L M₂) y ^ k) n = f m
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: case refine_1
R : 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✝⁴ : LieRing.IsNilpotent L
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective ⇑f
m : M
hm : m ∈ LieSubmodule.comap f (genWeightSpace M₂ χ)
⊢ m ∈ genWeightSpace M χ

Tactic:
simp only [LieSubmodule.mem_comap, mem_genWeightSpace] at hm
    simp only [mem_genWeightSpace]
    intro x
    have h : (toEnd R L M₂ x - χ x • ↑1) ∘ₗ f =
             f ∘ₗ (toEnd R L M x - χ x • ↑1) := by ext; simp
    obtain ⟨k, hk⟩ := hm x
    use k
    suffices f (((toEnd R L M x - χ x • ↑1) ^ k) m) = 0 by
      rw [← map_zero f] at this; exact hf this
    simpa [hk] using (LinearMap.congr_fun (Module.End.commute_pow_left_of_commute h k) m).symm

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : 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✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
⊢ IsCompl (genWeightSpace M 0) (posFittingComp R L M)

Tactic:
let P : LieSubmodule R L M → Prop := fun N ↦ IsCompl (genWeightSpace N 0) (posFittingComp R L N)

Goal state after:
R : 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✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
P : LieSubmodule R L M → Prop := fun N ↦ IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
⊢ IsCompl (genWeightSpace M 0) (posFittingComp R L M)
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K
hs : ∑ i ∈ s, w i • v i = 0
i : n
⊢ i ∈ s → w i = 0

Tactic:
hi

Goal state after:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
⊢ w i = 0
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case refine_1
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : (B x) x ≠ 0
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm : ∀ (y : ↥(B.orthogonal (K ∙ x))), ((B.restrict (B.orthogonal (K ∙ x))) m) y = 0
y : V
hy : y ∈ K ∙ x
z : V
hz : z ∈ B.orthogonal (K ∙ x)
⊢ (B ↑m) (y + z) = 0

Tactic:
add_right,

Goal state after:
case refine_1
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : (B x) x ≠ 0
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm : ∀ (y : ↥(B.orthogonal (K ∙ x))), ((B.restrict (B.orthogonal (K ∙ x))) m) y = 0
y : V
hy : y ∈ K ∙ x
z : V
hz : z ∈ B.orthogonal (K ∙ x)
⊢ (B ↑m) y + (B ↑m) z = 0
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map ↑I.incl ↑J;
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
this : J' = ⊥
⊢ J = ⊥

Tactic:
by
      rw [eq_bot_iff] at this ⊢
      intro x hx
      suffices x ∈ J → x = 0 from this hx
      have := @this x.1
      simp only [LieIdeal.incl_coe, LieIdeal.toLieSubalgebra_toSubmodule,
        LieSubmodule.mem_mk_iff', Submodule.mem_map, LieSubmodule.mem_toSubmodule, Subtype.exists,
        LieSubmodule.mem_bot, ZeroMemClass.coe_eq_zero, forall_exists_index, and_imp, J'] at this
      exact fun _ ↦ this (↑x) x.property hx rfl

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
A : Matrix ι ι R
⊢ (∀ (m : ι → R), ∃ n, (toLin' A ^ n) m = 0) ↔ ∀ (v : ι → R), ∃ n, A ^ n *ᵥ v = 0

Tactic:
← toLin'_pow,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
A : Matrix ι ι R
⊢ (∀ (m : ι → R), ∃ n, (toLin' (A ^ n)) m = 0) ↔ ∀ (v : ι → R), ∃ n, A ^ n *ᵥ v = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hm : m ∈ (f.genEigenspace μ) k
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
⊢ g m = μ • m

Tactic:
rw [f.mem_genEigenspace] at hm

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hm : ∃ l, ↑l ≤ k ∧ m ∈ ((f - μ • 1) ^ l).ker
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
⊢ g m = μ • m
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
y z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
⊢ ⁅y, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
induction hy using lieSpan_induction generalizing z with

Goal state after: