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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : ¬p = 0
⊢ rootMultiplicity x p ≤ 1

Tactic:
rootMultiplicity_eq_multiplicity,

Goal state after:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : ¬p = 0
⊢ (if p = 0 then 0 else multiplicity (X - C x) p) ≤ 1
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: M : Type u_1
p : ℕ
inst✝¹ : CommMonoid M
inst✝ : PerfectRing M p
n✝ n : ℕ
ih : powMulEquiv M (p ^ n) = powMulEquiv M p ^ n
⊢ powMulEquiv M (p ^ n.succ) = powMulEquiv M p ^ n.succ

Tactic:
by
    rw [pow_succ (powMulEquiv M p), ← ih, MulAut.mul_def, ← powMulEquiv_mul]
    congr
    rw [pow_succ']

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
p : ℕ
inst✝³ : ExpChar R p
inst✝² : PerfectRing R p
inst✝¹ : ExpChar S p
inst✝ : PerfectRing S p
f : R →* S
x : R
⊢ f ((frobeniusEquiv R p).symm x) = (frobeniusEquiv S p).symm (f x)

Tactic:
by
  apply_fun (frobeniusEquiv S p)
  simp [← MonoidHom.map_frobenius]

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case prime.inr
K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
hp : Nat.Prime p
hchar✝ : CharP K p
g : K[X]
hf : Irreducible ((expand K p) g)
⊢ ((expand K p) g).Separable

Tactic:
· exfalso; revert hf; have := Fact.mk hp; simp

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : ((expand F (p ^ k)) g₂).Separable
hgf₁ : (expand F (p ^ n₁)) ((expand F (p ^ k)) g₂) = f
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂

Tactic:
subst hgf₁

Goal state after:
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hg₁ : ((expand F (p ^ k)) g₂).Separable
hf : Irreducible ((expand F (p ^ n₁)) ((expand F (p ^ k)) g₂))
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) g₂ = g₂
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
H : (X ^ p - C y).roots = p • {(iterateFrobeniusEquiv R p 1).symm y}
⊢ (X ^ p - C y).roots = p • {(frobeniusEquiv R p).symm y}

Tactic:
iterateFrobeniusEquiv_one

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
H : (X ^ p - C y).roots = p • {(frobeniusEquiv R p).symm y}
⊢ (X ^ p - C y).roots = p • {(frobeniusEquiv R p).symm y}
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
m : ℕ
H : ((X ^ p - C y) ^ m).roots = (m * p) • {(iterateFrobeniusEquiv R p 1).symm y}
⊢ ((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}

Tactic:
iterateFrobeniusEquiv_one

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
m : ℕ
H : ((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}
⊢ ((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}
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✝¹ : DecidableEq R
inst✝ : PerfectRing R p
⊢ ⇑(frobeniusEquiv R p).toEquiv '' ↑((expand R p) f).roots.toFinset = ↑f.roots.toFinset

Tactic:
← roots_expand_image_frobenius (p := p) (f := f)

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p n : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : DecidableEq R
inst✝ : PerfectRing R p
⊢ ⇑(frobeniusEquiv R p).toEquiv '' ↑((expand R p) f).roots.toFinset =
    ↑(Finset.image (⇑(frobenius R p)) ((expand R p) f).roots.toFinset)
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : 𝕜[X]
a : A
⊢ p ∈ annIdeal 𝕜 a ↔ p ∈ 𝕜[X] ∙ annIdealGenerator 𝕜 a

Tactic:
← span_singleton_annIdealGenerator 𝕜 a

Goal state after:
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ annIdealGenerator 𝕜 a = minpoly 𝕜 a

Tactic:
rw [h, minpoly.eq_zero]
    rintro ⟨p, p_monic, hp : aeval a p = 0⟩
    refine p_monic.ne_zero (Ideal.mem_bot.mp ?_)
    simpa only [annIdealGenerator_eq_zero_iff.mp h] using mem_annIdeal_iff_aeval_eq_zero.mpr hp

Goal state after:
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
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ (aeval ⟨x, ⋯⟩) (minpoly R x) = 0

Tactic:
simp [← Subalgebra.coe_eq_zero, aeval_subalgebra_coe]

Goal state after:
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
⊢ f.IsFinitelySemisimple ↔
    ∀ p ∈ f.invtSubmodule,
      Module.Finite R ↥p → ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p

Tactic:
simp_rw [isFinitelySemisimple_iff', isSemisimple_restrict_iff]

Goal state after:
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
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
g : End R M₂
e : M ≃ₗ[R] M₂
he : ↑e ∘ₗ f = g ∘ₗ ↑e
x : M
⊢ (e ≪≫ₗ AEval'.of g) (f • x) = X • (e ≪≫ₗ AEval'.of g) x

Tactic:
by
    simpa [AEval'.X_smul_of] using LinearMap.congr_fun he x

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
x✝ : ↥R[x]
y₁ : S
y₂ : y₁ ∈ R[x]
h : ⟨y₁, y₂⟩ ∈ Subtype.val ⁻¹' {x}
⊢ (toAdjoin R x).toRingHom ((mk (minpoly R x)) X) = ⟨y₁, y₂⟩

Tactic:
by simpa using h.symm

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_1
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ eval₂ (↑(Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p)))))
      (1 ⊗ₜ[R] root p) (Polynomial.map (↑includeRight) p) =
    0

Tactic:
rw [Polynomial.eval₂_map]

Goal state after:
case refine_1
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ eval₂
      ((↑(Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))).comp
        ↑includeRight)
      (1 ⊗ₜ[R] root p) p =
    0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_1
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ eval₂
      ((Algebra.TensorProduct.map (AlgHom.id R T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p)))).comp
          includeRight).toRingHom
      (1 ⊗ₜ[R] root p) p =
    0

Tactic:
simp only [map_comp_includeRight, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom,
      AlgHom.coe_restrictScalars, ← Polynomial.eval₂_map]

Goal state after:
case refine_1
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ eval₂ (↑includeRight) (1 ⊗ₜ[R] root p) (Polynomial.map (↑(ofId S (AdjoinRoot p))) p) = 0
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: case succ
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ antidiagonal n
⊢ n.choose (i, j).1 • ⁅D ((⇑D)^[(i, j).1] a), (⇑D)^[(i, j).2] b⁆ =
    n.choose (i, j).2 • ⁅D ((⇑D)^[(i, j).1] a), (⇑D)^[(i, j).2] b⁆

Tactic:
n.choose_symm_of_eq_add (mem_antidiagonal.1 hij).symm

Goal state after:
case succ
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
a b : L
n : ℕ
ih : (⇑D)^[n] ⁅a, b⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ antidiagonal n
⊢ n.choose (i, j).2 • ⁅D ((⇑D)^[(i, j).1] a), (⇑D)^[(i, j).2] b⁆ =
    n.choose (i, j).2 • ⁅D ((⇑D)^[(i, j).1] a), (⇑D)^[(i, j).2] b⁆
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 : LieDerivation R L L
a b : L
⊢ ⁅a, D1 (D2 b)⁆ + ⁅D1 a, D2 b⁆ + (⁅D2 a, D1 b⁆ + ⁅D1 (D2 a), b⁆) -
      (⁅a, D2 (D1 b)⁆ + ⁅D2 a, D1 b⁆ + (⁅D1 a, D2 b⁆ + ⁅D2 (D1 a), b⁆)) =
    ⁅a, D1 (D2 b)⁆ - ⁅a, D2 (D1 b)⁆ - -(⁅D1 (D2 a), b⁆ - ⁅D2 (D1 a), b⁆)

Tactic:
abel

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 e f : LieDerivation R L L
a : L
⊢ d (f a) + e (f a) - (f (d a) + f (e a)) = d (f a) - f (d a) + (e (f a) - f (e a))

Tactic:
abel

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 e f : LieDerivation R L L
a : L
⊢ d (e a) + d (f a) - (e (d a) + f (d a)) = d (e a) - e (d a) + (d (f a) - f (d a))

Tactic:
abel

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
a : L
⊢ d (d a) - d (d a) = 0

Tactic:
abel

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 e f : LieDerivation R L L
a : L
⊢ d (e (f a)) - d (f (e a)) - (e (f (d a)) - f (e (d a))) =
    d (e (f a)) - e (d (f a)) - (f (d (e a)) - f (e (d a))) + (e (d (f a)) - e (f (d a)) - (d (f (e a)) - f (d (e a))))

Tactic:
abel

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y z : L
⊢ -(⁅⁅z, x⁆, y⁆ + -⁅⁅z, y⁆, x⁆) = - -⁅⁅z, y⁆, x⁆ - - -⁅⁅z, x⁆, y⁆

Tactic:
abel

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
⊢ ∃ S x x_1, ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits

Tactic:
by
  induction hn : p.natDegree using Nat.strong_induction_on generalizing R with | h n IH =>
  by_cases hpu : IsUnit p
  · obtain rfl := hp.eq_one_of_isUnit hpu
    exact ⟨R, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance, by simp⟩
  obtain ⟨q, hq⟩ : X - C (AdjoinRoot.root p) ∣ p.map (algebraMap _ _) := by
    simp [dvd_iff_isRoot, -AdjoinRoot.algebraMap_eq]
  have hqm : q.Monic := .of_mul_monic_left (monic_X_sub_C (.root _)) (hq ▸ hp.map _)
  have := hp.free_adjoinRoot
  have := hp.finite_adjoinRoot
  have : Nontrivial (AdjoinRoot p) := Ideal.Quotient.nontrivial_iff.mpr (by simpa)
  obtain ⟨S, _, _, _, _, _, hS⟩ := IH _
    (by rw [← hn, ← hp.natDegree_map (algebraMap R (AdjoinRoot p)), hq,
      Monic.natDegree_mul (monic_X_sub_C _) hqm]; simp) hqm rfl
  algebraize [(algebraMap (AdjoinRoot p) S).comp (algebraMap R (AdjoinRoot p))]
  refine ⟨S, ‹_›, ‹_›, .trans (AdjoinRoot p) _, .trans (S := AdjoinRoot p), ‹_›, ?_⟩
  rw [IsScalarTower.algebraMap_eq R (AdjoinRoot p), ← Polynomial.map_map, hq, Polynomial.map_mul]
  exact .mul (by simp) hS

Goal state after:
Module: Mathlib.LinearAlgebra.JordanChevalley

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
f : End K V
inst✝¹ : FiniteDimensional K V
inst✝ : PerfectField K
g : K[X]
k : ℕ
sep : Squarefree g
nil : minpoly K f ∣ g ^ k
⊢ ∃ n ∈ K[f], ∃ s ∈ K[f], IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Tactic:
rw [← PerfectField.separable_iff_squarefree] at sep

Goal state after:
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
f : End K V
inst✝¹ : FiniteDimensional K V
inst✝ : PerfectField K
g : K[X]
k : ℕ
sep : g.Separable
nil : minpoly K f ∣ g ^ k
⊢ ∃ n ∈ K[f], ∃ s ∈ K[f], IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
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
⊢ (LinearMap.rTensor N ((toEnd R L M) x)) t + (LinearMap.rTensor N ((toEnd R L M) y)) t +
      ((LinearMap.lTensor M ((toEnd R L N) x)) t + (LinearMap.lTensor M ((toEnd R L N) y)) t) =
    (LinearMap.rTensor N ((toEnd R L M) x)) t + (LinearMap.lTensor M ((toEnd R L N) x)) t +
      ((LinearMap.rTensor N ((toEnd R L M) y)) t + (LinearMap.lTensor M ((toEnd R L N) y)) t)

Tactic:
abel

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
⊢ ⁅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⁆⁆))

Tactic:
abel

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 : L
f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
⊢ ⁅x, (f m) n⁆ - (f m) ⁅x, n⁆ - (f ⁅x, m⁆) n = ⁅x, (f m) n⁆ - ((f ⁅x, m⁆) n + (f m) ⁅x, n⁆)

Tactic:
abel

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

Goal state before:
pp: case h.left
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : 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
I : LieIdeal R L
N : LieSubmodule R L M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ x ⊗ₜ[R] n ∈ {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t}

Tactic:
use ⟨x, hx⟩, ⟨n, hn⟩; rfl

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

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
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
⊢ ∃ k, derivedSeries R L k = ⊥

Tactic:
apply hL'.imp

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
hL' : ∃ k, derivedSeries R L' k = ⊥
h : Surjective ⇑f
⊢ ∀ (a : ℕ), derivedSeries R L' a = ⊥ → derivedSeries R L a = ⊥
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
⊢ ¬Nontrivial ↥(lowerCentralSeriesLast R L M)

Tactic:
rw [h.eq_bot, le_bot_iff] at this

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
h : Disjoint (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M)
a✝ : Nontrivial M
contra : ¬IsTrivial L M
this : lowerCentralSeriesLast R L M = ⊥
⊢ ¬Nontrivial ↥(lowerCentralSeriesLast R L M)
Module: Mathlib.FieldTheory.Finiteness

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hbfinite : (Basis.ofVectorSpaceIndex K V).Finite
⊢ span K ↑hbfinite.toFinset = ⊤

Tactic:
Set.Finite.coe_toFinset,

Goal state after:
case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hbfinite : (Basis.ofVectorSpaceIndex K V).Finite
⊢ span K (Basis.ofVectorSpaceIndex K V) = ⊤
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
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁ ≤ N₂
k : ℕ
ih : ucs k N₁ ≤ ucs k N₂
⊢ ucs (k + 1) N₁ ≤ ucs (k + 1) N₂

Tactic:
simp only [ucs_succ]
    gcongr

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
N₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
⊢ l + (k + 1) = l + 1 + k

Tactic:
abel

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)
x : ↥(subfield M F)
⊢ m • Polynomial.C x = Polynomial.C x

Tactic:
rw [Polynomial.smul_C, smul]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case inr
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * minpoly G F x = 1 * minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x g = 0
hg3 : g = minpoly G F x
⊢ f = 1

Tactic:
mul_left_inj' (monic G F x).ne_zero

Goal state after:
case inr
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f = 1
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x g = 0
hg3 : g = minpoly G F x
⊢ f = 1
Module: Mathlib.RingTheory.Adjoin.Dimension

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

Tactic:
← rank_lt_aleph0_iff,

Goal state after:
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A✝ B✝ A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
hA : ¬Module.rank R ↥A < Cardinal.aleph0
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B
Module: Mathlib.RingTheory.Adjoin.Field

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

Tactic:
eval_map

Goal state after:
case refine_2
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : (map (algebraMap F L) (minpoly F a)).Splits
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, (map (algebraMap F L) (minpoly F x)).Splits
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ (map (algebraMap F L) (minpoly F x)).Splits) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
this✝¹ : FiniteDimensional F ↥Ks
this✝ : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra (↥Ks) L := (↑f).toAlgebra
H5 : IsIntegral (↥Ks) a
H6 : (map (algebraMap (↥Ks) L) (minpoly (↥Ks) a)).Splits
y : L
hy : eval₂ (algebraMap (↥Ks) L) y (minpoly (↥Ks) a) = 0
⊢ Nonempty (↥(Subalgebra.restrictScalars F (↥Ks)[a]) →ₐ[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
L₁ L₂ : Lifts F E K
⊢ L₁ = L₂ ↔ ∃ (h : L₁.carrier = L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb

Tactic:
by
  rw [eq_iff_le_carrier_eq, le_iff]
  exact ⟨fun h ↦ ⟨h.2, h.1.2⟩, fun h ↦ ⟨⟨h.1.le, h.2⟩, h.1⟩⟩

Goal state after: