mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p n : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : PerfectRing R p
inst✝ : DecidableEq R
⊢ Finset.image (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots.toFinset = f.roots.toFinset

Tactic:
by
  rw [Finset.image_toFinset, roots_expand_pow_map_iterateFrobenius,
    (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne']

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
f : M ≃ₗ[A] M
⊢ LinearMap.det ↑f * LinearMap.det ↑f.symm = 1

Tactic:
by
  simp [← LinearMap.det_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
f : M ≃ₗ[A] M
⊢ LinearMap.det ↑f.symm * LinearMap.det ↑f = 1

Tactic:
by
  simp [← LinearMap.det_comp]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
h : Commute a b
⊢ (ad R A) ⁅a, b⁆ = 0

Tactic:
Ring.lie_def,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
h : Commute a b
⊢ (ad R A) (a * b - b * a) = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ≥0
x : AdjoinRoot f
p : K[X]
⊢ q • (mk f) p = (of f) ↑q * (mk f) p

Tactic:
simp only [smul_mk, of, RingHom.comp_apply, ← (mk f).map_mul, Polynomial.nnqsmul_eq_C_mul]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
⊢ minpoly K (root f) = f * C f.leadingCoeff⁻¹

Tactic:
refine (minpoly.unique K _ f'_monic ?_ ?_).symm

Goal state after:
case refine_1
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
⊢ (aeval (root f)) (f * C f.leadingCoeff⁻¹) = 0

case refine_2
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
⊢ ∀ (q : K[X]), q.Monic → (aeval (root f)) q = 0 → (f * C f.leadingCoeff⁻¹).degree ≤ q.degree
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hli
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * C f.leadingCoeff⁻¹
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
⊢ LinearIndependent K fun i ↦ root f ^ ↑i

Tactic:
exact linearIndependent_pow (root f)

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D1 D2 d : LieDerivation R L L
⊢ ⁅d, d⁆ = 0

Tactic:
by
    ext a; simp only [commutator_apply, zero_apply]; abel

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

Goal state before:
pp: case calc_3.i_inj
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 : ℕ := ⋯
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := ⋯
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := ⋯
hRN : RN = range (N + 1)
⊢ ∀ (a₁ : (_ : ℕ) × ℕ) (ha₁ : a₁ ∈ (range (2 * N + 1)).sigma fun i ↦ range (i + 1)) (a₂ : (_ : ℕ) × ℕ)
    (ha₂ : a₂ ∈ (range (2 * N + 1)).sigma fun i ↦ range (i + 1)),
    ((match a₁, ha₁ with
        | ⟨i, j⟩, x => (j, i - j)) =
        match a₂, ha₂ with
        | ⟨i, j⟩, x => (j, i - j)) →
      a₁ = a₂

Tactic:
simp only [mem_sigma, mem_range, Prod.mk.injEq, and_imp]

Goal state after:
case calc_3.i_inj
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)
⊢ ∀ (a₁ : (_ : ℕ) × ℕ),
    a₁.fst < 2 * N + 1 →
      a₁.snd < a₁.fst + 1 →
        ∀ (a₂ : (_ : ℕ) × ℕ),
          a₂.fst < 2 * N + 1 → a₂.snd < a₂.fst + 1 → a₁.snd = a₂.snd → a₁.fst - a₁.snd = a₂.fst - a₂.snd → a₁ = a₂
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case neg
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)
⊢ ∃ S x x_1, ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits

Tactic:
have := hp.finite_adjoinRoot

Goal state after:
case neg
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)
⊢ ∃ S x x_1, ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits
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 : ∀ (x : L), x ∈ ↑↑(derivedSeriesOfIdeal R L k ⊤) ↔ x ∈ ↑↑(derivedSeriesOfIdeal ℤ L k ⊤)
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ derivedSeriesOfIdeal R L k ⊤, ∃ n ∈ derivedSeriesOfIdeal R L k ⊤, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})

Tactic:
simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule] at ih

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

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

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

Tactic:
· exact LieAlgebra.isSolvableBot R L

Goal state after:
case refine_2
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
I✝ J✝ : LieIdeal R L
f : L' →ₗ⁅R⁆ L
inst✝ : IsNoetherian R L
hwf : CompleteLattice.IsSupClosedCompact (LieSubmodule R L L)
I : LieSubmodule R L L
hI : I ∈ {I | IsSolvable ↥I}
J : LieSubmodule R L L
hJ : J ∈ {I | IsSolvable ↥I}
⊢ I ⊔ J ∈ {I | IsSolvable ↥I}
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 : ∀ (x : M), x ∈ ↑↑(lowerCentralSeries R L M k) ↔ x ∈ ↑↑(lowerCentralSeries ℤ L M k)
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

Tactic:
simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule] at ih

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
k : ℕ
ih : ∀ (x : M), x ∈ lowerCentralSeries R L M k ↔ x ∈ lowerCentralSeries ℤ L M k
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries R L M k, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ ⊤, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R (↥I) k = ⊥}
s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
⊢ k ∈ s₁ ↔ k ∈ s₂

Tactic:
exact I.derivedSeries_eq_bot_iff k

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

Goal state before:
pp: case succ.refine_1
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 : ℕ
ih : ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
⊢ Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ Submodule.map ((toEnd R L M) x) ↑(I.lcs M (j + 1)) ≤
    Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑⁅I, I.lcs M j⁆

Tactic:
←
        I.lcs_succ

Goal state after:
case succ.refine_1
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 : ℕ
ih : ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
⊢ Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ Submodule.map ((toEnd R L M) x) ↑(I.lcs M (j + 1)) ≤
    Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
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
⊢ g • ∑ x ∈ s, (fun y ↦ l y • (toFun G F) y) x (g⁻¹ * g') = ∑ x ∈ s, (fun y ↦ l y • (toFun G F) y) x g'

Tactic:
← sum_apply _ _ fun y => l y • toFun G F y,

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
⊢ g • (∑ c ∈ s, l c • (toFun G F) c) (g⁻¹ * g') = ∑ x ∈ s, (fun y ↦ l y • (toFun G F) y) x g'
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f : Polynomial ↥(subfield G F)
hf : Polynomial.eval₂ (subfield G F).subtype x f = 0
y : G ⧸ stabilizer G x
g : G
⊢ Polynomial.X - Polynomial.C (ofQuotientStabilizer G x ↑g) ∣ Polynomial.map (subfield G F).subtype f

Tactic:
Polynomial.dvd_iff_isRoot,

Goal state after:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f : Polynomial ↥(subfield G F)
hf : Polynomial.eval₂ (subfield G F).subtype x f = 0
y : G ⧸ stabilizer G x
g : G
⊢ (Polynomial.map (subfield G F).subtype f).IsRoot (ofQuotientStabilizer G x ↑g)
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
x : E
hx : IsAlgebraic F x
⊢ ∀ x_1 ∈ {x}, IsAlgebraic F x_1

Tactic:
by simp [hx]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit ((aeval a) (Multiset.map (fun x ↦ X - C x) p.roots).toList.prod)
⊢ ∃ k ∈ σ a, eval k p = 0

Tactic:
map_list_prod

Goal state after:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit (List.map (⇑(aeval a)) (Multiset.map (fun x ↦ X - C x) p.roots).toList).prod
⊢ ∃ k ∈ σ a, eval k p = 0
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Ring K
inst✝² : IsDomain K
hk : IsAlgClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsIntegral k K
⊢ Function.Bijective ⇑(algebraMap k K)

Tactic:
refine ⟨RingHom.injective _, fun x ↦ ⟨-(minpoly k x).coeff 0, ?_⟩⟩

Goal state after:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Ring K
inst✝² : IsDomain K
hk : IsAlgClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsIntegral k K
x : K
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x
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
⊢ x ∈ adjoin F S ↔ ∃ r s, x = (MvPolynomial.aeval Subtype.val) r / (MvPolynomial.aeval Subtype.val) s

Tactic:
rw [← mem_adjoin_range_iff, Subtype.range_coe]

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

Goal state before:
pp: case empty
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst✝ : ∀ (i : ι), FiniteDimensional K ↥(t i)
x✝ : Set ι
⊢ FiniteDimensional K ↥(⨆ x ∈ ∅, t x)

Tactic:
| empty =>

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] (f : End K V),
      finrank K V = m → ⨆ μ, f.maxGenEigenspace μ = ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀) ↑(finrank K V)
ER : Submodule K V := f.genEigenrange μ₀ ↑(finrank K V)
h_f_ER : ∀ x ∈ ER, f x ∈ ER
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K ↥ES
h_dim_add : finrank K ↥ER + finrank K ↥ES = finrank K V
h_dim_ER : finrank K ↥ER < n.succ
ih_ER : ⨆ μ, f'.maxGenEigenspace μ = ⊤
ih_ER' : ⨆ μ, Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
μ✝ : K
⊢ Submodule.map ER.subtype (Submodule.comap ER.subtype ((f.genEigenspace μ✝) ⊤)) ≤ f.maxGenEigenspace μ✝

Tactic:
apply Submodule.map_comap_le

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
ι : Type u_3
f : ι → IntermediateField F E
x : E
hx : x ∈ ⨆ i, f i
⊢ ∃ s, x ∈ ⨆ i ∈ s, f i

Tactic:
by
  have := (adjoin_simple_isCompactElement x).exists_finset_of_le_iSup (IntermediateField F E) f
  simp only [adjoin_simple_le_iff] at this
  exact this hx

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case empty
ι : 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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ : ι → R
⊢ χ₁ ∉ ∅ → Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (∅.sup fun χ ↦ ⨅ i, (f i).maxGenEigenspace (χ i))

Tactic:
| empty =>

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
μ' : K
x✝ : μ' ∈ m.support.erase μ
this : MapsTo ⇑(f - (algebraMap K (End K V)) μ') ↑p ↑p
⊢ MapsTo ⇑((f - (algebraMap K (End K V)) μ') ^ l₀) ↑p ↑p

Tactic:
simp only [Module.End.coe_pow, this.iterate l₀]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h e f x : L
t : IsSl2Triple h e f
⊢ x ∈ toLieSubalgebra R t ↔ ∃ c₁ c₂ c₃, x = c₁ • e + c₂ • f + c₃ • h

Tactic:
toLieSubalgebra,

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h e f x : L
t : IsSl2Triple h e f
⊢ x ∈ { toSubmodule := Submodule.span R {e, f, h}, lie_mem' := ⋯ } ↔ ∃ c₁ c₂ c₃, x = c₁ • e + c₂ • f + c₃ • h
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: K : Type u_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
x : L
φ : Module.End R M := (toEnd R L M) x
y : L
k N : ℕ
hN : ∀ (x : L), (LieAlgebra.ad R L) x ^ N = 0
m : M
hm : ∀ (i : ℕ), ∃ y, (φ ^ i) y = (φ ^ (N + k)) m
f₁ : Module.End R (L ⊗[R] M) := LinearMap.rTensor M ((LieAlgebra.ad R L) x)
⊢ ∃ y_1, (φ ^ k) y_1 = ⁅y, (φ ^ (N + k)) m⁆

Tactic:
let f₂ : Module.End R (L ⊗[R] M) := φ.lTensor L

Goal state after:
K : Type u_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
x : L
φ : Module.End R M := (toEnd R L M) x
y : L
k N : ℕ
hN : ∀ (x : L), (LieAlgebra.ad R L) x ^ N = 0
m : M
hm : ∀ (i : ℕ), ∃ y, (φ ^ i) y = (φ ^ (N + k)) m
f₁ : Module.End R (L ⊗[R] M) := LinearMap.rTensor M ((LieAlgebra.ad R L) x)
f₂ : Module.End R (L ⊗[R] M) := LinearMap.lTensor L φ
⊢ ∃ y_1, (φ ^ k) y_1 = ⁅y, (φ ^ (N + k)) m⁆
Module: Mathlib.Algebra.Lie.Weights.Cartan

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
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
this : rootSpace H 0 ≤ H.toLieSubmodule
⊢ zeroRootSubalgebra R L H ≤ H

Tactic:
exact fun x hx => this hx

Goal state after:
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:
rw [dualBasis_repr_apply, dualBasis_repr_apply, apply_dualBasis_left, h]

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

Goal state before:
pp: k : Type u_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✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : CharZero R
χ : L → R
hχ : genWeightSpace M χ ≠ ⊥
x y : L
⊢ (LinearMap.trace R ↥(genWeightSpace M χ)) ⁅(toEnd R L ↥(genWeightSpace M χ)) x, (toEnd R L ↥(genWeightSpace M χ)) y⁆ =
    0

Tactic:
Ring.lie_def,

Goal state after:
k : Type u_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✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : CharZero R
χ : L → R
hχ : genWeightSpace M χ ≠ ⊥
x y : L
⊢ (LinearMap.trace R ↥(genWeightSpace M χ))
      ((toEnd R L ↥(genWeightSpace M χ)) x * (toEnd R L ↥(genWeightSpace M χ)) y -
        (toEnd R L ↥(genWeightSpace M χ)) y * (toEnd R L ↥(genWeightSpace M χ)) x) =
    0
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst ≠ v
⊢ count x.fst (v ::ₘ m) = count x.fst m

Tactic:
by simp [hx]

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✝ : HasTrivialRadical R L
⊢ IsLieAbelian ↥(radical R L)

Tactic:
HasTrivialRadical.radical_eq_bot

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : HasTrivialRadical R L
⊢ IsLieAbelian ↥⊥
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Algebra R A
inst✝⁴ : Module R M₁
inst✝³ : Module A M₁
inst✝² : SMulCommClass R A M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ IsSymm (B₁.tmul B₂)

Tactic:
by
  rw [LinearMap.isSymm_iff_eq_flip]
  ext x₁ x₂ y₁ y₂
  exact congr_arg₂ (HSMul.hSMul) (hB₂.eq x₂ y₂) (hB₁.eq x₁ y₁)

Goal state after: