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

Goal state before:
pp: case refine_2
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
ι : Sort u_1
N : ι → LieSubmodule R L M
motive : (x : M) → x ∈ ⨆ i, N i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : x ∈ ⨆ i, N i
⊢ ∃ (hx : 0 ∈ ⨆ i, N i), motive 0 hx

Tactic:
exact ⟨_, zero⟩

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
f : B →ₐ[A] B'
hf : Injective ⇑f
x : B
⊢ (if h : IsIntegral A x then ⋯.min (fun x_1 ↦ x_1.Monic ∧ (aeval (f x)) x_1 = 0) ⋯ else 0) =
    if hx : IsIntegral A x then ⋯.min (fun x_1 ↦ x_1.Monic ∧ (aeval x) x_1 = 0) ⋯ else 0

Tactic:
aeval_algHom,

Goal state after:
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
f : B →ₐ[A] B'
hf : Injective ⇑f
x : B
⊢ (if h : IsIntegral A x then ⋯.min (fun x_1 ↦ x_1.Monic ∧ (f.comp (aeval x)) x_1 = 0) ⋯ else 0) =
    if hx : IsIntegral A x then ⋯.min (fun x_1 ↦ x_1.Monic ∧ (aeval x) x_1 = 0) ⋯ else 0
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
⊢ p = minpoly A x

Tactic:
have hx : IsIntegral A x := ⟨p, hm, hp⟩

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
hm : p.Monic
hp : (Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0
a✝ : Nontrivial A
hx : IsIntegral A x
⊢ p = minpoly A x
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : (Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : c.natDegree ≤ 0
⊢ IsUnit 1

Tactic:
exact isUnit_one

Goal state after:
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: case cons
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
ι : Type u_6
x y : ι → M
i : ι
s : Finset ι
h✝ : i ∉ s
ih : (∀ i ∈ s, x i ≡ y i [SMOD U]) → ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U]
hxy : ∀ i_1 ∈ Finset.cons i s h✝, x i_1 ≡ y i_1 [SMOD U]
⊢ ∑ i ∈ Finset.cons i s h✝, x i ≡ ∑ i ∈ Finset.cons i s h✝, y i [SMOD U]

Tactic:
Finset.sum_cons,

Goal state after:
case cons
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
ι : Type u_6
x y : ι → M
i : ι
s : Finset ι
h✝ : i ∉ s
ih : (∀ i ∈ s, x i ≡ y i [SMOD U]) → ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U]
hxy : ∀ i_1 ∈ Finset.cons i s h✝, x i_1 ≡ y i_1 [SMOD U]
⊢ x i + ∑ x_1 ∈ s, x x_1 ≡ ∑ i ∈ Finset.cons i s h✝, y i [SMOD U]
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: case cons
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
ι : Type u_6
x y : ι → M
i : ι
s : Finset ι
h✝ : i ∉ s
ih : (∀ i ∈ s, x i ≡ y i [SMOD U]) → ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U]
hxy : ∀ i_1 ∈ Finset.cons i s h✝, x i_1 ≡ y i_1 [SMOD U]
⊢ x i + ∑ x_1 ∈ s, x x_1 ≡ ∑ i ∈ Finset.cons i s h✝, y i [SMOD U]

Tactic:
Finset.sum_cons,

Goal state after:
case cons
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
ι : Type u_6
x y : ι → M
i : ι
s : Finset ι
h✝ : i ∉ s
ih : (∀ i ∈ s, x i ≡ y i [SMOD U]) → ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U]
hxy : ∀ i_1 ∈ Finset.cons i s h✝, x i_1 ≡ y i_1 [SMOD U]
⊢ x i + ∑ x_1 ∈ s, x x_1 ≡ y i + ∑ x ∈ s, y x [SMOD U]
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ Ideal.span {X} ≤ RingHom.ker constantCoeff

Tactic:
simp [Ideal.span_le]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
⊢ y ∈ Submodule.span R (Set.range fun i ↦ x ^ ↑i) ↔ ∃ f, f.natDegree < d ∧ y = (aeval x) f

Tactic:
by
  rw [mem_span_pow']
  constructor <;>
  · rintro ⟨f, h, hy⟩
    refine ⟨f, ?_, hy⟩
    by_cases hf : f = 0
    · simp only [hf, natDegree_zero, Polynomial.degree_zero] at h ⊢
      first | exact lt_of_le_of_ne (Nat.zero_le d) hd.symm | exact WithBot.bot_lt_coe d
    simpa [degree_eq_natDegree hf] using h

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
⊢ Ideal.span {C x, X - C y} = Ideal.span {X - C y} ⊔ Ideal.span {C x}

Tactic:
Ideal.span_insert,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ Ideal.span {C x} ⊔ Ideal.span {X - C y} = Ideal.span {X - C y} ⊔ Ideal.span {C x}
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
⊢ (norm R) ((algebraMap R S) x) = x ^ Fintype.card ι

Tactic:
have := Classical.decEq ι
  rw [norm_apply, ← det_toMatrix b, lmul_algebraMap]
  simp

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
hn : 0 < n
H : Irreducible (X ^ n - C 0)
this : n = 1
⊢ root X = 0

Tactic:
← mk_X,

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
hn : 0 < n
H : Irreducible (X ^ n - C 0)
this : n = 1
⊢ (mk X) X = 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : LinearMap.det f ≠ 1
H : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ Free R M

Tactic:
classical simp [LinearMap.coe_det, H] at hf

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p m n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
⊢ x = (iterateFrobeniusEquiv R p (n + m)) ((iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x))

Tactic:
iterateFrobeniusEquiv_add_apply,

Goal state after:
R : Type u_1
p m n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
⊢ x =
    (iterateFrobeniusEquiv R p n)
      ((iterateFrobeniusEquiv R p m) ((iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x)))
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : LinearMap.det f ≠ 1
H : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ Module.Finite R M

Tactic:
classical simp [LinearMap.coe_det, H] at hf

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
⊢ ((expand R p) f).roots = p • Multiset.map (⇑(frobeniusEquiv R p).symm) f.roots

Tactic:
conv_lhs => rw [← pow_one p, roots_expand_pow, iterateFrobeniusEquiv_eq_pow, pow_one]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
⊢ p • Multiset.map (⇑(frobeniusEquiv R p ^ 1).symm) f.roots = p • Multiset.map (⇑(frobeniusEquiv R p).symm) f.roots
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = i x
⊢ h = C h.leadingCoeff * (X - C x)

Tactic:
have h_ne_zero : h ≠ 0 := by
    rintro rfl
    exact not_separable_zero h_sep
  suffices (map i h).roots = {i x} from
    map_injective i i.injective (by simpa using h_splits.eq_X_sub_C_of_single_root this)
  apply Finset.mk.inj
  · change _ = {i x}
    rw [Finset.eq_singleton_iff_unique_mem]
    constructor
    · apply Finset.mem_mk.mpr
      · rw [mem_roots (show h.map i ≠ 0 from map_ne_zero h_ne_zero)]
        rw [IsRoot.def, ← eval₂_eq_eval_map, eval₂_hom, h_root]
        exact map_zero i
      · exact nodup_roots (Separable.map h_sep)
    · exact h_roots

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
⊢ e.det ⇑e = 1

Tactic:
by simp [e.det_apply]

Goal state after:
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
⊢ (aeval
        (((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯).comp
            (Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f})))
          p))
      (minpoly K ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f})) p)) =
    0

Tactic:
aeval_algHom,

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) ⋯).comp
            (Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f}))).comp
        (aeval p))
      (minpoly K ((Ideal.Quotient.mkₐ K (Ideal.span {minpoly K f})) p)) =
    0
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:
aeval_algHom,

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]
⊢ (φ.comp (aeval p)) (minpoly K p) = 0
Module: Mathlib.Algebra.Lie.AdjointAction.JordanChevalley

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : PerfectField K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
n s : Module.End K V
hc : Commute n s
hn : IsNilpotent n
hs : s.IsSemisimple
n' : Module.End K (Module.End K V)
hn'_adj : n' ∈ K[(ad K (Module.End K V)) (n + s)]
s' : Module.End K (Module.End K V)
hs'_adj : s' ∈ K[(ad K (Module.End K V)) (n + s)]
hn'_nil : IsNilpotent n'
hs'_ss : s'.IsSemisimple
h_jc : (ad K (Module.End K V)) (n + s) = n' + s'
hc' : Commute n' s'
hs_eq : s' = (ad K (Module.End K V)) s
⊢ (ad K (Module.End K V)) s ∈ K[(ad K (Module.End K V)) (n + s)]

Tactic:
rwa [hs_eq] at hs'_adj

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

Goal state before:
pp: 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
x y : L
t : M ⊗[R] N
m : M
n : N
⊢ ((AlgebraTensorModule.curry (hasBracketAux x ∘ₗ hasBracketAux y)) m) n =
    ((AlgebraTensorModule.curry (hasBracketAux ⁅x, y⁆ + hasBracketAux y ∘ₗ hasBracketAux x)) m) n

Tactic:
simp only [hasBracketAux, AlgebraTensorModule.curry_apply, curry_apply, sub_tmul, tmul_sub,
      LinearMap.coe_restrictScalars, Function.comp_apply, LinearMap.coe_comp,
      LinearMap.rTensor_tmul, LieHom.map_lie, toEnd_apply_apply, LinearMap.add_apply,
      map_add, LieHom.lie_apply, Module.End.lie_apply, LinearMap.lTensor_tmul]

Goal state after:
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
x y : L
t : M ⊗[R] N
m : M
n : N
⊢ ⁅x, ⁅y, m⁆⁆ ⊗ₜ[R] n + ⁅y, m⁆ ⊗ₜ[R] ⁅x, n⁆ + (⁅x, m⁆ ⊗ₜ[R] ⁅y, n⁆ + m ⊗ₜ[R] ⁅x, ⁅y, n⁆⁆) =
    ⁅x, ⁅y, m⁆⁆ ⊗ₜ[R] n - ⁅y, ⁅x, m⁆⁆ ⊗ₜ[R] n + (m ⊗ₜ[R] ⁅x, ⁅y, n⁆⁆ - m ⊗ₜ[R] ⁅y, ⁅x, n⁆⁆) +
      (⁅y, ⁅x, m⁆⁆ ⊗ₜ[R] n + ⁅x, m⁆ ⊗ₜ[R] ⁅y, n⁆ + (⁅y, m⁆ ⊗ₜ[R] ⁅x, n⁆ + m ⊗ₜ[R] ⁅y, ⁅x, n⁆⁆))
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 J : LieIdeal R L
k l : ℕ
h₁ : I ≤ J
h₂ : l ≤ k
⊢ D k I ≤ D l J

Tactic:
by
  induction k generalizing l with
  | zero => rw [le_zero_iff] at h₂; rw [h₂, derivedSeriesOfIdeal_zero]; exact h₁
  | succ k ih =>
    have h : l = k.succ ∨ l ≤ k := by rwa [le_iff_eq_or_lt, Nat.lt_succ_iff] at h₂
    rcases h with h | h
    · rw [h, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]
      exact LieSubmodule.mono_lie (ih (le_refl k)) (ih (le_refl k))
    · rw [derivedSeriesOfIdeal_succ]; exact le_trans (LieSubmodule.lie_le_left _ _) (ih h)

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

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

Tactic:
apply isUnit_iff_exists.2

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
h : IsNilpotent a
⊢ ∃ b, exp a * b = 1 ∧ b * exp a = 1
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
⊢ IsLieAbelian ↥I ↔ D 1 I = ⊥

Tactic:
rw [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero,
    LieSubmodule.lie_abelian_iff_lie_self_eq_bot]

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:
simp only [lcs_succ]

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
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lcs k N ≤ N
⊢ ⁅⊤, lcs k N⁆ ≤ N
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
⊢ derivedSeries R L (k + 1) ≤ lowerCentralSeries R L L (k + 1)

Tactic:
have h' : derivedSeries R L k ≤ ⊤ := by simp only [le_top]

Goal state after:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
h' : derivedSeries R L k ≤ ⊤
⊢ derivedSeries R L (k + 1) ≤ lowerCentralSeries R L L (k + 1)
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
⊢ derivedSeries R L (k + 1) ≤ lowerCentralSeries R L L (k + 1)

Tactic:
have h' : derivedSeries R L k ≤ ⊤ := by simp only [le_top]
    rw [derivedSeries_def, derivedSeriesOfIdeal_succ, lowerCentralSeries_succ]
    exact LieSubmodule.mono_lie h' h

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

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
⊢ ⊤ ∈ s

Tactic:
have _i5 : IsNoetherian R L' := by
    refine isNoetherian_of_surjective (LieHom.rangeRestrict (toEnd R L M)).toLinearMap ?_
    simp only [LinearMap.range_eq_top]
    exact LieHom.surjective_rangeRestrict (toEnd R L M)

Goal state after:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
_i5 : IsNoetherian R ↥L'
⊢ ⊤ ∈ s
Module: Mathlib.Algebra.Lie.Nilpotent

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
inst✝ : IsNilpotent L M
⊢ IsNilpotent (A ⊗[R] L) (A ⊗[R] M)

Tactic:
obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R L M
  rw [isNilpotent_iff A]
  exact ⟨k, by simp [hk]⟩

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case f
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 : F
| g • (l x * (g⁻¹ * g') • x)

Tactic:
← toFun_apply _ x

Goal state after:
case f
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 : F
| g • (l x * (toFun G F) x (g⁻¹ * g'))
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
f : K[X]
inst✝ : IsSplittingField K L f
h : ⊤ = ⊥
⊢ f.Splits

Tactic:
by
    rw [← Polynomial.map_id (p := f), ← RingEquiv.toRingHom_refl, ← RingEquiv.self_trans_symm
      (RingEquiv.ofBijective _ <| Algebra.bijective_algebraMap_iff.2 h),
      RingEquiv.toRingHom_trans, ← map_map]
    apply (splits L f).map

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
y : F
⊢ (algebraMap (↥⊥) E) ((botEquiv F E).symm y) = (algebraMap F E) ((botEquiv F E) ((botEquiv F E).symm y))

Tactic:
(botEquiv F E).apply_symm_apply,

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
y : F
⊢ (algebraMap (↥⊥) E) ((botEquiv F E).symm y) = (algebraMap F E) y
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: L : Type u_2
inst✝ : Field L
F : Subfield L
x : L
⊢ x ∈ F ↔ x ∈ ⊥

Tactic:
IntermediateField.mem_bot

Goal state after:
L : Type u_2
inst✝ : Field L
F : Subfield L
x : L
⊢ x ∈ F ↔ x ∈ Set.range ⇑(algebraMap (↥F) L)
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₂ L₃ : Lifts F E K
h₁₂ : L₁.carrier ≤ L₂.carrier
h₁₂' : ∀ (x : ↥L₁.carrier), L₂.emb ((inclusion h₁₂) x) = L₁.emb x
h₂₃ : L₂.carrier ≤ L₃.carrier
h₂₃' : ∀ (x : ↥L₂.carrier), L₃.emb ((inclusion h₂₃) x) = L₂.emb x
x✝ : ↥L₁.carrier
⊢ L₃.emb ((inclusion h₂₃) ((inclusion h₁₂) x✝)) = L₁.emb x✝

Tactic:
h₂₃',

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₂ L₃ : Lifts F E K
h₁₂ : L₁.carrier ≤ L₂.carrier
h₁₂' : ∀ (x : ↥L₁.carrier), L₂.emb ((inclusion h₁₂) x) = L₁.emb x
h₂₃ : L₂.carrier ≤ L₃.carrier
h₂₃' : ∀ (x : ↥L₂.carrier), L₃.emb ((inclusion h₂₃) x) = L₂.emb x
x✝ : ↥L₁.carrier
⊢ L₂.emb ((inclusion h₁₂) x✝) = L₁.emb 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:
← mem_adjoin_range_iff,

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
⊢ x ∈ adjoin F S ↔ x ∈ adjoin F (Set.range Subtype.val)
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: case h
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
f : End R M
k : ℕ∞
hf : ⨆ μ, (f.genEigenspace μ) k = ⊤
this : ∃ μ, f.HasUnifEigenvalue μ k
μ : R
hμ : f.HasUnifEigenvalue μ k
⊢ f.HasEigenvalue μ

Tactic:
exact HasUnifEigenvalue.lt zero_lt_one hμ

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.snd⟯

Tactic:
refine exists_finset_of_mem_iSup (SetLike.le_def.mp (iSup_le fun i x h ↦ ?_) hx)
  exact SetLike.le_def.mp (le_iSup_of_le ⟨i, x, h⟩ (by simp)) (mem_adjoin_simple_self F x)

Goal state after: