mathlib-initiative/mathlib-tactics huggingface dataset:
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
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = r.leadingCoeff
hr0 : r ≠ 0
hr : (minpoly A x).natDegree = (p * r).natDegree
⊢ r.natDegree ≤ 0

Tactic:
hm.natDegree_mul' hr0

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
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = r.leadingCoeff
hr0 : r ≠ 0
hr : (minpoly A x).natDegree = p.natDegree + r.natDegree
⊢ r.natDegree ≤ 0
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: case inl
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
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = r.leadingCoeff
this : r.natDegree ≤ 0
⊢ p = p * r

Tactic:
eq_C_of_natDegree_le_zero this,

Goal state after:
case inl
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
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = r.leadingCoeff
this : r.natDegree ≤ 0
⊢ p = p * C (r.coeff 0)
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
⊢ map f ⁅I₁, I₂⁆ ≤ ⁅map f I₁, map f I₂⁆

Tactic:
rw [map_le_iff_le_comap, LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I₁ I₂ : LieIdeal R L
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑(comap f ⁅map f I₁, map f I₂⁆)
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
p : A[X]
hi : Irreducible p
b : B
hfa : (Polynomial.aeval b) p = 0
g : A[X]
⊢ (Polynomial.aeval b) (p * g) = 0

Tactic:
simp [hfa]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
⊢ RingHom.ker (evalRingHom x) = Ideal.span {X - C x}

Tactic:
ext y

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
y : R[X]
⊢ y ∈ RingHom.ker (evalRingHom x) ↔ y ∈ Ideal.span {X - C x}
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
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f g : S →ₐ[R] S'
h : f pb.gen = g pb.gen
x : S
⊢ f x = g x

Tactic:
obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f✝ g : S →ₐ[R] S'
h : f✝ pb.gen = g pb.gen
f : R[X]
⊢ f✝ ((aeval pb.gen) f) = g ((aeval pb.gen) f)
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
⊢ ((C.comp (Quotient.mk I)) (a.coeff n)).coeff m = coeff 0 m

Tactic:
rw [RingHom.comp_apply, coeff_C]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
⊢ (if m = 0 then (Quotient.mk I) (a.coeff n) else 0) = coeff 0 m
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ Function.RightInverse ⇑(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))

Tactic:
rintro ⟨f⟩

Goal state after:
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
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
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
x x' : S
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) (x * x') =
    ((pb.basis.constr A) fun i ↦ y ^ ↑i) x * ((pb.basis.constr A) fun i ↦ y ^ ↑i) x'

Tactic:
obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x

Goal state after:
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
x' : S
f : A[X]
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) f * x') =
    ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) f) * ((pb.basis.constr A) fun i ↦ y ^ ↑i) x'
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : (aeval pb.gen) (minpoly A (pb.map e).gen) = 0
h₂ : (aeval (pb.map e).gen) (minpoly A pb.gen) = 0
x : S
⊢ (pb.equivOfRoot (pb.map e) h₁ h₂) x = e x

Tactic:
obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x

Goal state after:
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : (aeval pb.gen) (minpoly A (pb.map e).gen) = 0
h₂ : (aeval (pb.map e).gen) (minpoly A pb.gen) = 0
f : A[X]
⊢ (pb.equivOfRoot (pb.map e) h₁ h₂) ((aeval pb.gen) f) = e ((aeval pb.gen) f)
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ 2 ≤ emultiplicity a r ↔ 1 < emultiplicity a r

Tactic:
← one_add_one_eq_two

Goal state after:
R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ 1 + 1 ≤ emultiplicity a r ↔ 1 < emultiplicity a r
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
z w : R
h0 : z * z * w ≠ 0
h : IsRadical (z * z * w)
⊢ (z * w) ^ 2 = z * z * w * w

Tactic:
simp_rw [pow_two, mul_left_comm, ← mul_assoc]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
h : derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
⊢ f ∣ derivative f

Tactic:
conv_lhs => rw [hg3, ← hu]

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
h : derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
⊢ g * ↑u ∣ derivative f
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
inst✝ : DecidableEq M
⊢ ⇑LinearMap.det = ⇑(if H : ∃ s, Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1)

Tactic:
by
  ext
  rw [LinearMap.det_def]
  split_ifs
  · congr -- use the correct `DecidableEq` instance
  rfl

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: M : Type u_1
p q : ℕ
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
inst✝ : PerfectRing M q
⊢ Bijective fun x ↦ x ^ (p * q)

Tactic:
simp_rw [pow_mul]; exact PerfectRing.bijective_frobenius.comp PerfectRing.bijective_frobenius

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case neg
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ¬∃ s, Nonempty (Basis (↥s) A M)
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f

Tactic:
have H' : ¬∃ t : Finset N, Nonempty (Basis t A N) := by
        contrapose H
        rcases H with ⟨s, ⟨b⟩⟩
        exact ⟨_, ⟨(b.map e.symm).reindexFinsetRange⟩⟩
      simp only [coe_det, H, H', MonoidHom.one_apply, dif_neg, not_false_eq_true]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : (of f) p = 0
⊢ p = 0

Tactic:
AdjoinRoot.of,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : ((mk f).comp C) p = 0
⊢ p = 0
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_5
inst✝ : Finite ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
h : f ⇑e = 0
⊢ f = 0

Tactic:
cases nonempty_fintype ι
    let := Classical.decEq ι
    simpa [h] using f.eq_smul_basis_det e

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
w : ι → Rˣ
⊢ (e.unitsSMul w).det = ↑(∏ i, w i)⁻¹ • e.det

Tactic:
ext f

Goal state after:
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
w : ι → Rˣ
f : ι → M
⊢ (e.unitsSMul w).det f = (↑(∏ i, w i)⁻¹ • e.det) f
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
⊢ LinearMap.det e = LinearMap.det (e.restrict he) * LinearMap.det (W.mapQ W e he)

Tactic:
let m := Module.Free.ChooseBasisIndex R W

Goal state after:
R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
⊢ LinearMap.det e = LinearMap.det (e.restrict he) * LinearMap.det (W.mapQ W e he)
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ (∀ (a : Submodule R M) (b : a ∈ ((Algebra.lsmul R R M) f).invtSubmodule),
      a ≤ p →
        ∃ a_2,
          ∃ (h : a_2 ∈ ((Algebra.lsmul R R M) f).invtSubmodule), a_2 ≤ p ∧ ⟨a ⊓ a_2, ⋯⟩ = ⊥ ∧ ⟨a ⊔ a_2, ⋯⟩ = ⟨p, hp⟩) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p

Tactic:
Subtype.mk.injEq,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ (∀ (a : Submodule R M) (b : a ∈ ((Algebra.lsmul R R M) f).invtSubmodule),
      a ≤ p → ∃ a_2, ∃ (h : a_2 ∈ ((Algebra.lsmul R R M) f).invtSubmodule), a_2 ≤ p ∧ ⟨a ⊓ a_2, ⋯⟩ = ⊥ ∧ a ⊔ a_2 = p) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: case refine_2
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
a : End K M
ha : a ∈ K[f, g]
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
⊢ ∀ (a : R), Commute ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) a) g

Tactic:
rintro ⟨p⟩

Goal state after:
case refine_2.mk
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
a : End K M
ha : a ∈ K[f, g]
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
a✝ : R
p : K[X]
⊢ Commute
    ((Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯)
      (Quot.mk (⇑(Submodule.quotientRel (Ideal.span {minpoly K f}))) p))
    g
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
x : L
D₁ D₂ : LieDerivation R L L
⊢ ⁅x, ⁅D₁, D₂⁆⁆ = ⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆

Tactic:
ext y

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D₁ D₂ : LieDerivation R L L
y : L
⊢ ⁅x, ⁅D₁, D₂⁆⁆ y = (⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆) y
Module: Mathlib.Dynamics.Newton

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : (aeval x) P = 0
⊢ IsFixedPt P.newtonMap x

Tactic:
rw [IsFixedPt, newtonMap_apply, h, mul_zero, sub_zero]

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

Goal state before:
pp: case smul_mem
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R₁
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R₁ L
inst✝⁴ : LieAlgebra R₂ L
inst✝³ : Module R₁ M
inst✝² : Module R₂ M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x | ∃ a, ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
c : R₁
y : M
hy : y ∈ S
⊢ c • y ∈ Submodule.span R₂ S

Tactic:
obtain ⟨a, b, hb, rfl⟩ := hy
      rw [← smul_lie]
      exact Submodule.subset_span ⟨c • a, b, hb, rfl⟩

Goal state after:
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
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s

Tactic:
intro k₁

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k₁ : ℕ
⊢ ∀ (k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: case succ.refine_2
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))
⊢ ↑⁅I, ⊤.lcs M (i + l)⁆ ≤ ↑⁅I, I.lcs M j⁆

Tactic:
· norm_cast
      gcongr
      exact le_trans (antitone_lowerCentralSeries R L M le_self_add) hIM

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

Goal state before:
pp: case H.H
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
z✝¹ z✝ : L
⊢ (↑f).quotKerEquivRange ⁅Submodule.Quotient.mk z✝¹, Submodule.Quotient.mk z✝⁆ =
    ⁅(↑f).quotKerEquivRange (Submodule.Quotient.mk z✝¹), (↑f).quotKerEquivRange (Submodule.Quotient.mk z✝)⁆

Tactic:
← SetLike.coe_eq_coe,

Goal state after:
case H.H
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
z✝¹ z✝ : L
⊢ ↑((↑f).quotKerEquivRange ⁅Submodule.Quotient.mk z✝¹, Submodule.Quotient.mk z✝⁆) =
    ↑⁅(↑f).quotKerEquivRange (Submodule.Quotient.mk z✝¹), (↑f).quotKerEquivRange (Submodule.Quotient.mk z✝)⁆
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
this : ∀ (l : ℕ), lowerCentralSeries R L M (l * n) ≤ I.lcs M l
⊢ LieModule.IsNilpotent L M

Tactic:
rw [isNilpotent_iff R]
    use k * n
    simpa [hk'] using this k

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

Goal state before:
pp: R : Type u₁
L : Type u₂
L₂ : Type u₃
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective ⇑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)
this✝ : LieRingModule L M := LieRingModule.compLieHom M f
this : LieModule R L M := compLieHom M f
hnp : ∀ (x : L), IsNilpotent ((toEnd R L M) x)
surj_id : Surjective ⇑LinearMap.id
⊢ LieModule.IsNilpotent L₂ M

Tactic:
have : LieModule.IsNilpotent L M := h M hnp

Goal state after:
R : Type u₁
L : Type u₂
L₂ : Type u₃
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective ⇑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)
this✝¹ : LieRingModule L M := LieRingModule.compLieHom M f
this✝ : LieModule R L M := compLieHom M f
hnp : ∀ (x : L), IsNilpotent ((toEnd R L M) x)
surj_id : Surjective ⇑LinearMap.id
this : LieModule.IsNilpotent L M
⊢ LieModule.IsNilpotent L₂ M
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
h : Disjoint (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
a✝ : Nontrivial M
contra : ¬IsTrivial L M
this✝ : lowerCentralSeriesLast R L M ≤ lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M
this : ¬Nontrivial ↥(lowerCentralSeriesLast R L M)
⊢ False

Tactic:
by
    exact this (nontrivial_lowerCentralSeriesLast R L M)

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

Goal state before:
pp: case succ
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
⊢ Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅x_1, n⁆ = x} =
    Submodule.span R {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅x_1, n⁆ = x}

Tactic:
(I : LieSubalgebra R L).coe_bracket_of_module

Goal state after:
case succ
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k✝ : ℕ
inst✝ : LieModule R L M
k : ℕ
ih : ↑(I.lcs M k) = ↑(lowerCentralSeries R (↥I) M k)
⊢ Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅x_1, n⁆ = x} =
    Submodule.span R {x | ∃ x_1, ∃ n ∈ lowerCentralSeries R (↥I) M k, ⁅↑x_1, n⁆ = x}
Module: Mathlib.RingTheory.Adjoin.Dimension

Goal state before:
pp: case neg.inr
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
this :
  ∀ (A B : Subalgebra R S) [Free R ↥A] [Free R ↥B],
    ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B) → ¬Module.Finite R ↥A → finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B
hA : ¬¬Module.Finite R ↥A
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
have := this B A (fun h' ↦ h h'.symm) (not_and.1 h (of_not_not hA))
    rwa [sup_comm, mul_comm] at this

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.IsSplittingField

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
f : K[X]
inst✝ : IsSplittingField K L f
hf : (Polynomial.map (algebraMap K F) f).Splits
hf0 : ¬f = 0
⊢ ↥⊤ →ₐ[K] F

Tactic:
by
    rw [← adjoin_rootSet L f]
    exact Classical.choice (lift_of_splits _ fun y hy =>
      have : aeval y f = 0 := (eval₂_eq_eval_map _).trans <|
        (mem_roots <| map_ne_zero hf0).1 (Multiset.mem_toFinset.mp hy)
    ⟨IsAlgebraic.isIntegral ⟨f, hf0, this⟩, hf.of_dvd (map_ne_zero hf0)
      ((map_dvd_map' _).mpr (minpoly.dvd K y this))⟩)

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
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ * x✝², ⋯⟩ = φ₂ ⟨x✝³ * x✝², ⋯⟩

Tactic:
convert! congr_arg₂ (· * ·) h₁ h₂

Goal state after:
case e'_2
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ * x✝², ⋯⟩ = φ₁ ⟨x✝³, x✝¹⟩ * φ₁ ⟨x✝², x✝⟩

case e'_3
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₂ ⟨x✝³ * x✝², ⋯⟩ = φ₂ ⟨x✝³, x✝¹⟩ * φ₂ ⟨x✝², x✝⟩