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

Goal state before:
pp: case inl
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ (i.1 ≤ N → N < i.2)
h : N + 1 ≤ i.1
⊢ ((↑i.1!)⁻¹ * (↑i.2!)⁻¹) • (a ^ i.1 * b ^ i.2) = 0

Tactic:
| inl h =>

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
⊢ exp 0 = 1

Tactic:
by
  simp [exp_eq_sum (pow_one 0)]

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
h : derivedSeries R L 1 = ⊤
n✝ : ℕ
⊢ derivedSeries R L (n✝ + 1) = ⊤

Tactic:
· rwa [derivedSeries_succ_eq_top_iff]

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

Goal state before:
pp: 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
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule) x
⊢ y ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)

Tactic:
rintro ⟨z, hz⟩

Goal state after:
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
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule) x
z : L
hz : z ∈ H
⊢ ⁅⟨z, hz⟩, y⁆ = 0
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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x' : L ⧸ I
⊢ ⁅x', x'⁆ = 0

Tactic:
induction x' using Quotient.inductionOn' with

Goal state after:
case h
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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x : L
⊢ ⁅Quotient.mk'' x, Quotient.mk'' x⁆ = 0
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:
rw [Set.mem_ofPred_eq] at hI hJ ⊢

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 : IsSolvable ↥I
J : LieSubmodule R L L
hJ : IsSolvable ↥J
⊢ IsSolvable ↥(I ⊔ J)
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
N : LieSubmodule R L M
x : A ⊗[R] L
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
⊢ ⁅x, m⁆ ∈ Submodule.baseChange A ↑N

Tactic:
obtain ⟨c, rfl⟩ := (Finsupp.mem_span_iff_linearCombination _ _ _).mp hm

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
N : LieSubmodule R L M
x : A ⊗[R] L
c : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →₀ A
hm : (Finsupp.linearCombination A Subtype.val) c ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
⊢ ⁅x, (Finsupp.linearCombination A Subtype.val) c⁆ ∈ Submodule.baseChange A ↑N
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
⊢ IsNilpotent L (M ⧸ N) ↔ ∃ k, lowerCentralSeries R L M k ≤ N

Tactic:
rw [isNilpotent_iff R L]
  refine exists_congr fun k ↦ ?_
  rw [← LieSubmodule.Quotient.map_mk'_eq_bot_le, map_lowerCentralSeries_eq k
    (LieSubmodule.Quotient.surjective_mk' N)]

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

Goal state before:
pp: 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
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f : L ≃ₗ⁅R⁆ L₂
g : M ≃ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆
h : LieModule.IsNilpotent L M
⊢ LieModule.IsNilpotent L₂ M₂

Tactic:
have hg : Surjective (g : M →ₗ[R] M₂) := g.surjective
    exact f.surjective.lieModuleIsNilpotent hfg hg

Goal state after:
Module: Mathlib.FieldTheory.Tower

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝⁶ : Semiring F
inst✝⁵ : Semiring K
inst✝⁴ : Module F K
inst✝³ : AddCommMonoid A
inst✝² : Module K A
inst✝¹ : Module F A
inst✝ : IsScalarTower F K A
hf : Module.Finite F A
b : Finset A
hb : span F ↑b = ⊤
⊢ restrictScalars F (span K ↑b) = restrictScalars F ⊤

Tactic:
rw [Submodule.restrictScalars_top, eq_top_iff, ← hb, Submodule.span_le]
    exact Submodule.subset_span

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
inst✝ : FiniteDimensional (↥F) L
H : F < E
⊢ finrank (↥E) L < finrank (↥F) L

Tactic:
let := (IntermediateField.inclusion H.le).toAlgebra

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
H : F < E
this : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
⊢ finrank (↥E) L < finrank (↥F) L
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: case refine_2
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : (map (algebraMap F L) (minpoly F a)).Splits
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, (map (algebraMap F L) (minpoly F x)).Splits
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
this✝¹ : FiniteDimensional F ↥Ks
this✝ : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra (↥Ks) L := (↑f).toAlgebra
H5 : IsIntegral (↥Ks) a
H6 : (map (algebraMap (↥Ks) L) (minpoly (↥Ks) a)).Splits
⊢ Nonempty (↥(Subalgebra.restrictScalars F (↥Ks)[a]) →ₐ[F] L)

Tactic:
obtain ⟨y, hy⟩ := H6.exists_eval_eq_zero (by simp [(minpoly.degree_pos H5).ne'])

Goal state after:
case refine_2
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : (map (algebraMap F L) (minpoly F a)).Splits
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, (map (algebraMap F L) (minpoly F x)).Splits
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
this✝¹ : FiniteDimensional F ↥Ks
this✝ : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra (↥Ks) L := (↑f).toAlgebra
H5 : IsIntegral (↥Ks) a
H6 : (map (algebraMap (↥Ks) L) (minpoly (↥Ks) a)).Splits
y : L
hy : eval y (map (algebraMap (↥Ks) L) (minpoly (↥Ks) a)) = 0
⊢ Nonempty (↥(Subalgebra.restrictScalars F (↥Ks)[a]) →ₐ[F] L)
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hk : ¬IsUnit (↑ₐ k - (aeval a) p)
hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) (C k - p).roots).prod
h_ne : C k - p ≠ 0
lead_ne : (C k - p).leadingCoeff ≠ 0
lead_unit : IsUnit ↑((Units.map ↑↑ₐ) (Units.mk0 (C k - p).leadingCoeff lead_ne))
p_a_eq : (aeval a) (C k - p) = ↑ₐ k - (aeval a) p
⊢ k ∈ (fun x ↦ eval x p) '' σ a

Tactic:
← p_a_eq,

Goal state after:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < p.degree
k : 𝕜
hk : ¬IsUnit ((aeval a) (C k - p))
hprod : C k - p = C (C k - p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) (C k - p).roots).prod
h_ne : C k - p ≠ 0
lead_ne : (C k - p).leadingCoeff ≠ 0
lead_unit : IsUnit ↑((Units.map ↑↑ₐ) (Units.mk0 (C k - p).leadingCoeff lead_ne))
p_a_eq : (aeval a) (C k - p) = ↑ₐ k - (aeval a) p
⊢ k ∈ (fun x ↦ eval x p) '' σ a
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: case neg
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → ∃ x, eval x p = 0
p : k[X]
hp0 : ¬p = 0
u : k[X]ˣ
hu : (UniqueFactorizationMonoid.factors p).prod * ↑u = p
⊢ ((UniqueFactorizationMonoid.factors p).prod * ↑u).Splits

Tactic:
refine (Splits.multisetProd fun f hf ↦ ?_).mul u.isUnit.splits

Goal state after:
case neg
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → ∃ x, eval x p = 0
p : k[X]
hp0 : ¬p = 0
u : k[X]ˣ
hu : (UniqueFactorizationMonoid.factors p).prod * ↑u = p
f : k[X]
hf : f ∈ UniqueFactorizationMonoid.factors p
⊢ f.Splits
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝¹⁸ : Field k
K✝ : Type u
inst✝¹⁷ : Field K✝
L : Type v
M : Type w
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra K✝ L
inst✝¹⁴ : Field M
inst✝¹³ : Algebra K✝ M
inst✝¹² : IsAlgClosed M
inst✝¹¹ : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type v
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R M
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree R M
inst✝² : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := X ^ (n + 1) - 1
hfsep : f.Separable
⊢ n.succ = Fintype.card ↑(f.rootSet K)

Tactic:
rw [card_rootSet_eq_natDegree hfsep (IsAlgClosed.splits_domain _)]

Goal state after:
k : Type u
inst✝¹⁸ : Field k
K✝ : Type u
inst✝¹⁷ : Field K✝
L : Type v
M : Type w
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra K✝ L
inst✝¹⁴ : Field M
inst✝¹³ : Algebra K✝ M
inst✝¹² : IsAlgClosed M
inst✝¹¹ : Algebra.IsAlgebraic K✝ L
R : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type v
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R M
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree R M
inst✝² : Algebra.IsAlgebraic R S
K : Type u_1
inst✝¹ : Field K
inst✝ : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := X ^ (n + 1) - 1
hfsep : f.Separable
⊢ n.succ = f.natDegree
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

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
x : E
hx : x ∈ adjoin F S
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ adjoin F ↑T

Tactic:
← biSup_adjoin_simple S,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
hx : x ∈ ⨆ x ∈ S, F⟮x⟯
⊢ ∃ T, ↑T ⊆ S ∧ x ∈ adjoin F ↑T
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ Module.finrank K ↥K⟮x⟯ = (minpoly K x).natDegree

Tactic:
rw [PowerBasis.finrank (adjoin.powerBasis hx :)]
  rfl

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
α : E
K : Type u
inst✝³ : Field K
inst✝² : Algebra F K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
xt : ↥⊤ := ⟨x, ⋯⟩
⊢ IsAlgebraic (↥⊤) x

Tactic:
exact isAlgebraic_algebraMap xt

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra F K
hA : ∀ (x : K), (map (algebraMap F L) (minpoly F x)).Splits
inst✝ : Algebra.IsAlgebraic F K
x : K
a : L
⊢ (a ∈ Set.range fun ψ ↦ ψ x) ↔ a ∈ (minpoly F x).rootSet L

Tactic:
rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x))]

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra F K
hA : ∀ (x : K), (map (algebraMap F L) (minpoly F x)).Splits
inst✝ : Algebra.IsAlgebraic F K
x : K
a : L
⊢ (a ∈ Set.range fun ψ ↦ ψ x) ↔ (aeval a) (minpoly F x) = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
K : Type u_3
M : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun i j ↦ Commute (f i) (f j)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
i j : ι
⊢ Commute (f j) (f i)

Tactic:
rcases eq_or_ne j i with rfl | hij

Goal state after:
case inl
ι : Type u_1
K : Type u_3
M : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun i j ↦ Commute (f i) (f j)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
j : ι
⊢ Commute (f j) (f j)

case inr
ι : Type u_1
K : Type u_3
M : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun i j ↦ Commute (f i) (f j)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
i j : ι
hij : j ≠ i
⊢ Commute (f j) (f i)
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: ι : Type u_1
K : Type u_3
M : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun i j ↦ Commute (f i) (f j)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
i j : ι
⊢ Commute (f j) (f i)

Tactic:
rcases eq_or_ne j i with rfl | hij <;> tauto

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

Goal state before:
pp: case mem
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
H : LieSubalgebra R L
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
s : Set (↥H → R)
hs : ∀ χ₁ ∈ s, ∀ χ₂ ∈ s, χ₁ + χ₂ ∈ s
x : L
m : M
hm : m ∈ ⨆ χ ∈ s, genWeightSpace M χ
χ₁ : ↥H → R
u : L
hu : u ∈ ⨆ (_ : χ₁ ∈ s), rootSpace H χ₁
⊢ ⁅u, m⁆ ∈ ⨆ χ ∈ s, genWeightSpace M χ

Tactic:
by_cases hχ₁ : χ₁ ∈ s; swap
    · simp_all
    replace hu : u ∈ rootSpace H χ₁ := by simpa [hχ₁] using hu
    induction hm using LieSubmodule.iSup_induction' with
    | zero => simp
    | add _ _ _ _ hv hw => rw [lie_add]; exact add_mem hv hw
    | mem χ₂ v hv =>
      by_cases hχ₂ : χ₂ ∈ s; swap
      · simp_all
      apply LieSubmodule.mem_iSup_of_mem (χ₁ + χ₂)
      simp_all [lie_mem_genWeightSpace_of_mem_genWeightSpace]

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✝ : IsNilpotent L M
x : L
⊢ posFittingCompOf R M x ≤ ⨅ k, lowerCentralSeries R L M k

Tactic:
le_iInf_iff,

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✝ : IsNilpotent L M
x : L
⊢ ∀ (i : ℕ), posFittingCompOf R M x ≤ lowerCentralSeries R L M i
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
⊢ ⨅ k, lowerCentralSeries R L M k = posFittingComp R L M

Tactic:
refine le_antisymm ?_ (posFittingComp_le_iInf_lowerCentralSeries R L M)

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
⊢ ⨅ k, lowerCentralSeries R L M k ≤ posFittingComp R L M
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
i j : ι
this : FiniteDimensional K V
⊢ (b.coord i) (b j) = if j = i then 1 else 0

Tactic:
Basis.coord_apply,

Goal state after:
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
i j : ι
this : FiniteDimensional K V
⊢ (b.repr (b j)) i = if j = i then 1 else 0
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
v : ι → V
h : ∀ (i j : ι), (B (v i)) (b j) = if j = i then 1 else 0
x✝¹ x✝ : ι
⊢ ((B.dualBasis hB b).repr ((B.dualBasis hB b) x✝¹)) x✝ = ((B.dualBasis hB b).repr (v x✝¹)) x✝

Tactic:
by
      rw [dualBasis_repr_apply, dualBasis_repr_apply, apply_dualBasis_left, h]

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✝¹ : Nontrivial M
inst✝ : IsTriangularizable R L M
x : L
this : ⨆ φ, ((toEnd R L M) x).maxGenEigenspace φ = ⊤
⊢ ∃ φ, ((toEnd R L M) x).maxGenEigenspace φ ≠ ⊥

Tactic:
contrapose! this

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✝¹ : Nontrivial M
inst✝ : IsTriangularizable R L M
x : L
this : ∀ (φ : R), ((toEnd R L M) x).maxGenEigenspace φ = ⊥
⊢ ⨆ φ, ((toEnd R L M) x).maxGenEigenspace φ ≠ ⊤
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✝¹ : Nontrivial M
inst✝ : IsTriangularizable R L M
x : L
⊢ ∃ φ, ((toEnd R L M) x).HasEigenvalue φ

Tactic:
by
  suffices ∃ φ, (toEnd R L M x).maxGenEigenspace φ ≠ ⊥ by
    obtain ⟨φ, hφ⟩ := this
    exact ⟨φ, (Module.End.hasUnifEigenvalue_iff_hasUnifEigenvalue_one ENat.top_pos).mp hφ⟩
  have := maxGenEigenspace_eq_top (R := R) (L := L) (M := M) x
  contrapose! this
  simp [this]

Goal state after:
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✝ : IsSimple R L
this : ¬IsLieAbelian L
⊢ Nontrivial L

Tactic:
contrapose! this

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
this : Subsingleton L
⊢ IsLieAbelian L
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝² : Field k
K : Type ?u.6
inst✝¹ : Field K
inst✝ : DecidableEq K
i : k →+* K
f : Monics k
hf : (map i ↑f).Splits
⊢ (map i ↑f).roots.toEnumFinset.card = (↑f).natDegree

Tactic:
rwa [splits_iff_card_roots,
      ← Multiset.card_toEnumFinset, f.2.natDegree_map] at hf

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map (↑(toSplittingField s)) (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f) -
          ∏ x, (X - C (↑(toSplittingField s) (MvPolynomial.X ⟨f, x⟩)))).coeff
      n =
    0

Tactic:
toSplittingField,

Goal state after:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
h : f ∈ s
n : ℕ
⊢ (map (↑(MvPolynomial.aeval fun fi ↦ if hf : fi.fst ∈ s then (↑((finEquivRoots ⋯) fi.snd)).1 else 37))
            (map (algebraMap k (MvPolynomial (Vars k) k)) ↑f) -
          ∏ x,
            (X -
              C
                (↑(MvPolynomial.aeval fun fi ↦ if hf : fi.fst ∈ s then (↑((finEquivRoots ⋯) fi.snd)).1 else 37)
                  (MvPolynomial.X ⟨f, x⟩)))).coeff
      n =
    0
Module: Mathlib.Algebra.Lie.Weights.Chain

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz : z ∈ genWeightSpace M (↑⟨k, hk⟩ • α + χ)
this : genWeightSpace M ((k + 1) • α + χ) ≤ genWeightSpaceChain M α χ p q
⊢ α + (k • α + χ) = (k + 1) • α + χ

Tactic:
rw [add_smul]; abel

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' : ∀ y ∈ rootSpace H (-α), ((killingForm K L) x) y = 0
y : L
⊢ ((killingForm K L) x) y = 0 y

Tactic:
have hy : y ∈ ⨆ β, rootSpace H β := by simp [iSup_genWeightSpace_eq_top K H L]

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : ↥H → K
x : L
hx : x ∈ rootSpace H α
hx' : ∀ y ∈ rootSpace H (-α), ((killingForm K L) x) y = 0
y : L
hy : y ∈ ⨆ β, rootSpace H β
⊢ ((killingForm K L) x) y = 0 y