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

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : (Polynomial.aeval σ.toLinearMap) q = 0
⊢ ↑(orderOf σ) ≤ ↑q.natDegree

Tactic:
Nat.cast_le,

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
hs : (Polynomial.aeval σ.toLinearMap) q = 0
⊢ orderOf σ ≤ q.natDegree
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
⊢ minpoly K σ.toLinearMap = minpoly K ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit).toLinearMap

pp: case hσ
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
⊢ IsOfFinOrder ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)

Tactic:
· apply congr_arg
    ext
    simp

Goal state after:
case hσ
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
⊢ IsOfFinOrder ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
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 : ℕ
n : S
⊢ (∃ y, x ^ ↑y = n) ↔ ∃ x_1 ∈ ↑(Finset.range d), x ^ x_1 = n

Tactic:
Finset.mem_coe,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
n : S
⊢ (∃ y, x ^ ↑y = n) ↔ ∃ x_1 ∈ Finset.range d, x ^ x_1 = n
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
H : ∑ i, (pb.basis.repr b) i • pb.basis i = b
⊢ b ≡ (algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩) [SMOD Ideal.span {pb.gen}]

Tactic:
← insert_erase (mem_univ ⟨0, pb.dim_pos⟩),

Goal state after:
case inr
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
H : ∑ i ∈ insert ⟨0, ⋯⟩ (univ.erase ⟨0, ⋯⟩), (pb.basis.repr b) i • pb.basis i = b
⊢ b ≡ (algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩) [SMOD Ideal.span {pb.gen}]
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst✝ : Invertible x
h✝ : ∃ i ∈ Ideal.map (algebraMap R ↥R[x]) I, ∃ j ∈ Ideal.span {⟨x, ⋯⟩}, i + j = 1
y : ↥R[x]
hy : y ∈ Ideal.map (algebraMap R ↥R[x]) I
z : ↥R[x]
hz : z ∈ Ideal.span {⟨x, ⋯⟩}
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y
w : ↥R[x]
q : R[X]
hq : (aeval x) q = ↑w
this : (1 - p - X * q).coeff 0 - 1 ∈ I
eq : ↑y + ↑z = 1
hw : ↑z = ↑(⟨x, ⋯⟩ * w)
h : (1 - p - X * q).coeff 0 = 0
⊢ I = ⊤

Tactic:
by simpa [h, Ideal.eq_top_iff_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
⊢ (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
      ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) f) =
    f

Tactic:
refine Polynomial.induction_on' f ?_ ?_

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
⊢ ∀ (p q : (R ⧸ I)[X]),
    (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
          ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) p) =
        p →
      (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
            ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) q) =
          q →
        (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
            ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) (p + q)) =
          p + q

case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
⊢ ∀ (n : ℕ) (a : R ⧸ I),
    (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
        ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
          ((monomial n) a)) =
      (monomial n) a
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : p.natDegree < pb.dim
i : Fin pb.dim
root : ∑ x, p.coeff ↑x • pb.basis x = 0
this : ∀ (i : Fin pb.dim), p.coeff ↑i = 0
⊢ (monomial ↑i) (p.coeff ↑i) = 0

Tactic:
rw [this, monomial_zero_right]

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

Goal state before:
pp: case mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f : R[X]
⊢ (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
      ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
        (Quot.mk (⇑(Submodule.quotientRel (map C I))) f)) =
    Quot.mk (⇑(Submodule.quotientRel (map C I))) f

Tactic:
refine Polynomial.induction_on' f ?_ ?_

Goal state after:
case mk.refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f : R[X]
⊢ ∀ (p q : R[X]),
    (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
          ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
            (Quot.mk (⇑(Submodule.quotientRel (map C I))) p)) =
        Quot.mk (⇑(Submodule.quotientRel (map C I))) p →
      (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
            ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
              (Quot.mk (⇑(Submodule.quotientRel (map C I))) q)) =
          Quot.mk (⇑(Submodule.quotientRel (map C I))) q →
        (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
            ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
              (Quot.mk (⇑(Submodule.quotientRel (map C I))) (p + q))) =
          Quot.mk (⇑(Submodule.quotientRel (map C I))) (p + q)

case mk.refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f : R[X]
⊢ ∀ (n : ℕ) (a : R),
    (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
        ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
          (Quot.mk (⇑(Submodule.quotientRel (map C I))) ((monomial n) a))) =
      Quot.mk (⇑(Submodule.quotientRel (map C I))) ((monomial n) a)
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
r : R
⊢ eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) (C r)) =
    (Ideal.Quotient.mk (Ideal.map C I)) (C r)

Tactic:
eval₂Hom_C,

Goal state after:
case C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
r : R
⊢ eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯)
      (fun i ↦ (Ideal.Quotient.mk (Ideal.map C I)) (X i)) ((C.comp (Ideal.Quotient.mk I)) r) =
    (Ideal.Quotient.mk (Ideal.map C I)) (C r)
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: n : ℕ
⊢ Squarefree ↑n ↔ Squarefree n

Tactic:
rw [← squarefree_natAbs, natAbs_natCast]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
hnsep : ¬(GCDMonoid.gcd f (derivative f)).degree = 0
x : F
hx : eval x (GCDMonoid.gcd f (derivative f)) = 0
⊢ ∃ x, ¬Multiset.count x f.roots ≤ 1

Tactic:
not_le

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
hnsep : ¬(GCDMonoid.gcd f (derivative f)).degree = 0
x : F
hx : eval x (GCDMonoid.gcd f (derivative f)) = 0
⊢ ∃ x, 1 < Multiset.count x f.roots
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ C p
h : ¬f = 0
⊢ p = 0

Tactic:
contrapose! hf with h_contra

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ f.degree = 0
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b b' : Basis ι A M
⊢ LinearMap.det ↑(b.equiv b' (Equiv.refl ι)) * LinearMap.det ↑(b'.equiv b (Equiv.refl ι)) = 1

Tactic:
exact LinearEquiv.det_mul_det_symm _

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: 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 : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ ↑(f * C f.leadingCoeff⁻¹).natDegree ≤ ↑q.natDegree

Tactic:
Nat.cast_le,

Goal state after:
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 : q.Monic
q_aeval : (aeval (root f)) q = 0
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ (f * C f.leadingCoeff⁻¹).natDegree ≤ q.natDegree
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✝ : CommRing R
I : Ideal R
f : R[X]
⊢ Ideal.map (Ideal.Quotient.mk (Ideal.map C I)) (span {f}) = span {(Ideal.Quotient.mk (Ideal.map C I)) f}

Tactic:
by rw [map_span, Set.image_singleton]

Goal state after:
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)
this✝ : Module.Finite R (AdjoinRoot p)
this : Nontrivial (AdjoinRoot p)
S : Type u
w✝⁴ : CommRing S
w✝³ : Algebra (AdjoinRoot p) S
w✝² : Module.Finite (AdjoinRoot p) S
w✝¹ : Free (AdjoinRoot p) S
w✝ : Nontrivial S
hS : (Polynomial.map (algebraMap (AdjoinRoot p) S) q).Splits
algInst✝ : Algebra R S := ((algebraMap (AdjoinRoot p) S).comp (algebraMap R (AdjoinRoot p))).toAlgebra
scalarTowerInst✝ : IsScalarTower R (AdjoinRoot p) S := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S))
⊢ (Polynomial.map (algebraMap R S) p).Splits

Tactic:
IsScalarTower.algebraMap_eq R (AdjoinRoot p),

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)
this : Nontrivial (AdjoinRoot p)
S : Type u
w✝⁴ : CommRing S
w✝³ : Algebra (AdjoinRoot p) S
w✝² : Module.Finite (AdjoinRoot p) S
w✝¹ : Free (AdjoinRoot p) S
w✝ : Nontrivial S
hS : (Polynomial.map (algebraMap (AdjoinRoot p) S) q).Splits
algInst✝ : Algebra R S := ((algebraMap (AdjoinRoot p) S).comp (algebraMap R (AdjoinRoot p))).toAlgebra
scalarTowerInst✝ : IsScalarTower R (AdjoinRoot p) S := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S))
⊢ (Polynomial.map ((algebraMap (AdjoinRoot p) S).comp (algebraMap R (AdjoinRoot p))) p).Splits
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x + y) ^ n = 0
⊢ x ^ m ∣ y ^ p

Tactic:
by
  rw [← neg_neg y, neg_pow']
  apply dvd_mul_of_dvd_left
  apply h_comm.neg_right.pow_dvd_pow_of_sub_pow_eq_zero hp
  simpa

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
n : ℕ
ih : derivedSeriesOfIdeal R L (n + 1) ⊤ = ⊤ ↔ derivedSeriesOfIdeal R L 1 ⊤ = ⊤
h : ⁅derivedSeriesOfIdeal R L (n + 1) ⊤, derivedSeriesOfIdeal R L (n + 1) ⊤⁆ = ⊤
⊢ derivedSeriesOfIdeal R L (n + 1) ⊤ = ⊤

Tactic:
eq_top_iff

Goal state after:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
n : ℕ
ih : derivedSeriesOfIdeal R L (n + 1) ⊤ = ⊤ ↔ derivedSeriesOfIdeal R L 1 ⊤ = ⊤
h : ⁅derivedSeriesOfIdeal R L (n + 1) ⊤, derivedSeriesOfIdeal R L (n + 1) ⊤⁆ = ⊤
⊢ ⊤ ≤ derivedSeriesOfIdeal R L (n + 1) ⊤
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x y : L
hx : x ∈ {x | ∀ (m : M), ⁅x, m⁆ ∈ N}
hy : y ∈ {x | ∀ (m : M), ⁅x, m⁆ ∈ N}
m : M
⊢ ⁅x + y, m⁆ ∈ N

Tactic:
by rw [add_lie]; exact N.add_mem (hx m) (hy m)

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

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

Tactic:
apply le_antisymm

Goal state after:
case succ.a
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 ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x}) ⊆
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})

case a
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 ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x}) ⊆
    ↑(Submodule.span R {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})
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 ℤ L M k, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

Tactic:
apply le_antisymm

Goal state after:
case succ.a
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 ℤ L M k, ⁅x_1, n⁆ = x}) ⊆
    ↑(Submodule.span ℤ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x})

case a
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 ℤ {x | ∃ x_1, ∃ n ∈ lowerCentralSeries ℤ L M k, ⁅x_1, n⁆ = x}) ⊆
    ↑(Submodule.span R {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
inst✝ : IsSolvable L
⊢ radical R L = ⊤

Tactic:
eq_top_iff

Goal state after:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSolvable L
⊢ ⊤ ≤ radical R L
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
k✝ : ℕ
N✝ : LieSubmodule R L M
M₂✝ : Type w₁
inst✝⁶ : AddCommGroup M₂✝
inst✝⁵ : Module R M₂✝
inst✝⁴ : LieRingModule L M₂✝
inst✝³ : LieModule R L M₂✝
inst✝² : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst✝¹ : IsNilpotent L ↥M₁
inst✝ : IsNilpotent L ↥M₂
k : ℕ
hk : lowerCentralSeries R L (↥M₁) k = ⊥
l : ℕ
hl : lowerCentralSeries R L (↥M₂) l = ⊥
m n : ℕ
N : LieSubmodule R L M
le : m ≤ n
hn : lowerCentralSeries R L (↥N) m = ⊥
⊢ lowerCentralSeries R L (↥N) n = ⊥

Tactic:
by
    simpa [hn] using antitone_lowerCentralSeries R L N le

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

Goal state before:
pp: case h
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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥

Tactic:
suffices lowerCentralSeries R L M k ≤ N by
    replace this := LieSubmodule.mono_lie_right ⊤ (le_trans this h₁)
    rwa [ideal_oper_maxTrivSubmodule_eq_bot, le_bot_iff] at this

Goal state after:
case h
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
N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ lowerCentralSeries R L M k ≤ N
Module: Mathlib.FieldTheory.Finiteness

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
b : Basis (↥(finsetBasisIndex K V)) K V := finsetBasis K V
⊢ Nat.card V = Nat.card K ^ finrank K V

Tactic:
rw [Nat.card_congr b.equivFun.toEquiv, Nat.card_fun, finrank_eq_nat_card_basis b]

Goal state after:
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
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
⊢ maxNilpotentSubmodule R L M = ⊤

Tactic:
eq_top_iff

Goal state after:
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
inst✝ : IsNilpotent L M
⊢ ⊤ ≤ maxNilpotentSubmodule R L M
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : Normal F E
x : E
⊢ IsIntegral K x ∧ (map (algebraMap K E) (minpoly K x)).Splits

Tactic:
by
    obtain ⟨hx, hhx⟩ := h.out x
    rw [algebraMap_eq F K E, ← map_map] at hhx
    exact ⟨hx.tower_top, hhx.of_dvd (map_ne_zero (map_ne_zero (minpoly.ne_zero hx)))
      ((map_dvd_map' _).mpr (minpoly.dvd_map_of_isScalarTower F K x))⟩

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: M : Type u
inst✝² : Monoid M
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction M F
m : M
p : Polynomial ↥(subfield M F)
n : ℕ
x : ↥(subfield M F)
x✝ : m • (Polynomial.C x * Polynomial.X ^ n) = Polynomial.C x * Polynomial.X ^ n
⊢ m • (Polynomial.C x * Polynomial.X ^ (n + 1)) = Polynomial.C x * Polynomial.X ^ (n + 1)

Tactic:
by
    rw [smul_mul', Polynomial.smul_C, smul, smul_pow', Polynomial.smul_X]

Goal state after:
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_1
inst✝⁵ : Field F
E : Type u_3
inst✝⁴ : Field E
inst✝³ : Algebra F E
M : Type u_5
N : Type u_6
inst✝² : Field N
inst✝¹ : Field M
inst✝ : Algebra M N
h : Normal F E
f : F ≃+* M
g : E ≃+* N
hcomp : (algebraMap M N).comp ↑f = (↑g).comp (algebraMap F E)
⊢ Normal M N

Tactic:
have := h
  rw [normal_iff] at h ⊢
  intro x
  rw [← g.apply_symm_apply x]
  refine ⟨(h (g.symm x)).1.map_of_comp_eq _ _ hcomp, ?_⟩
  rw [← minpoly.map_eq_of_equiv_equiv hcomp, map_map, hcomp, ← map_map]
  exact (h (g.symm x)).2.map _

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case intro.right
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G = Fintype.card (F →ₐ[↥(subfield G F)] F)

Tactic:
apply le_antisymm

Goal state after:
case intro.right.a
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G ≤ Fintype.card (F →ₐ[↥(subfield G F)] F)

case a
G : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card (F →ₐ[↥(subfield G F)] F) ≤ Fintype.card 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
y : L
hy : y ∈ ↑(Finset.image (⇑(algebraMap K L)) f.roots.toFinset)
⊢ y ∈ ↑⊥

Tactic:
Finset.mem_coe,

Goal state after:
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
y : L
hy : y ∈ Finset.image (⇑(algebraMap K L)) f.roots.toFinset
⊢ y ∈ ↑⊥
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
S : Set (IntermediateField F E)
hS : S.Nonempty
⊢ (sSup S).toSubfield = sSup (toSubfield '' S)

Tactic:
have h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S := by
    rw [Set.image_image]
    congr! with x
    exact x.toSubfield.closure_eq.symm
  rw [h, sSup_image, ← Subfield.closure_sUnion, sSup_def, adjoin_toSubfield]
  congr 1
  rw [Set.union_eq_right]
  rintro _ ⟨x, rfl⟩
  obtain ⟨y, hy⟩ := hS
  simp only [Set.mem_sUnion, Set.mem_image, exists_exists_and_eq_and, SetLike.mem_coe]
  exact ⟨y, hy, algebraMap_mem y x⟩

Goal state after: