mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono

Goal state before:
pp: case h₁
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Epi (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯).τ₁

pp: case h₂
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯).τ₂

pp: case h₃
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Mono (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯).τ₃

Tactic:
· dsimp
    convert! (inferInstance : Epi ((X.H n₀).map (𝟙 _)))
    cat_disch

Goal state after:
case h₂
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯).τ₂

case h₃
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Mono (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯).τ₃
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R P
inst✝¹ : Module R N
ι : Type u_5
inst✝ : Finite ι
⊢ ∀ {α β : Type u_5} (a : α ≃ β),
    (∀ {M : α → Submodule R P} [∀ (i : α), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)) →
      ∀ {M : β → Submodule R P} [∀ (i : β), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)

Tactic:
intro _ _ e h _ _

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
ι : Type u_5
inst✝¹ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R P
inst✝ : ∀ (i : β✝), IsArtinian R ↥(M✝ i)
⊢ IsArtinian R ↥(⨆ i, M✝ i)
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
m : ℕ
hm : n ≤ m
x y : M
hy : (f ^ m) ((f ^ n) y) = (f ^ m) x
⊢ ∃ y ∈ (f ^ m).ker, ∃ z ∈ range (f ^ n), y + z = x

Tactic:
exact ⟨x - (f ^ n) y, by simp [hy], (f ^ n) y, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsArtinianRing R
x : R
⊢ IsUnit x ↔ IsRegular x

Tactic:
by
  rw [isRegular_iff, ← isUnit_iff_isRightRegular, and_iff_right_of_imp (·.isRegular.1)]

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝¹ :
  ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn✝ : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
ne : ∀ x ∈ N, I x = ⊥
ri : R
hi : ri ∈ Jac ^ n
rn : R
hn : rn ∈ N
⊢ ri * rn ∈ ⊥

Tactic:
← ne rn hn

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn✝¹ :
  ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
hn✝ : Jac * Jac ^ n = Jac ^ n
ne✝ : ¬Ring.jacobson R ^ n = 0
N : Ideal R
eq : Jac * N = N
min : ∀ x ∈ {N | Jac * N = N ∧ N ≠ ⊥}, ¬x < N
this : Jac ^ n * N = N
I : R → Submodule R R := fun x ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
ne : ∀ x ∈ N, I x = ⊥
ri : R
hi : ri ∈ Jac ^ n
rn : R
hn : rn ∈ N
⊢ ri * rn ∈ I rn
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: 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
N N' : LieSubmodule R L M
⊢ Codisjoint ↑N ↑N' ↔ Codisjoint N N'

Tactic:
by
  rw [codisjoint_iff, codisjoint_iff, ← toSubmodule_inj, sup_toSubmodule,
    top_toSubmodule, ← codisjoint_iff]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : IsReduced B
n : ℕ
p : A[X]
dvd : minpoly A x ∣ p ^ n
⊢ minpoly A x ∣ p

Tactic:
rw [dvd_iff] at dvd ⊢; rw [map_pow] at dvd; exact IsReduced.eq_zero _ ⟨n, dvd⟩

Goal state after:
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
h : Function.Surjective ⇑f
y₁ : ↥I₁
h₁ : f ↑y₁ ∈ map f I₁
y₂ : ↥I₂
h₂ : f ↑y₂ ∈ map f I₂
⊢ ↑f ⁅↑y₁, ↑y₂⁆ = ⁅↑⟨f ↑y₁, h₁⟩, ↑⟨f ↑y₂, h₂⟩⁆

Tactic:
by apply f.map_lie

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q

Tactic:
have : Polynomial.aeval x (p * q) = 0 := by simp [h, aeval A x]

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
this : (Polynomial.aeval x) (p * q) = 0
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ Function.LeftInverse ⇑(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:
by
    intro f
    refine Polynomial.induction_on' f ?_ ?_
    · intro p q hp hq
      simp only [coe_eval₂RingHom] at hp hq
      simp only [coe_eval₂RingHom, hp, hq, map_add]
    · rintro n ⟨x⟩
      simp only [← smul_X_eq_monomial, C_mul', Quotient.lift_mk, Submodule.Quotient.quot_mk_eq_mk,
        Quotient.mk_eq_mk, eval₂_X_pow, eval₂_smul, coe_eval₂RingHom, map_pow, eval₂_C,
        RingHom.coe_comp, map_mul, eval₂_X, Function.comp_apply]

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
⊢ False

Tactic:
have hd₀ : d ≠ 0 := ne_zero_of_dvd_ne_zero (ne_zero_of_dvd_ne_zero hx₀ hd) (dvd_mul_left d d)

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
hd₀ : d ≠ 0
⊢ False
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hsep : p.Separable
x : R
⊢ rootMultiplicity x p ≤ 1

Tactic:
exact rootMultiplicity_le_one_of_separable hsep x

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case h.inr.zero
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : f.coeff 0 = 0
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
ih : ∀ m < 0, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f = C 0
hf0 : f ≠ 0
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f

Tactic:
C_0

Goal state after:
case h.inr.zero
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : f.coeff 0 = 0
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
ih : ∀ m < 0, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f = 0
hf0 : f ≠ 0
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
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
⊢ (iterateFrobeniusEquiv R p (m + n)) ((iterateFrobeniusEquiv R p (m + n)).symm x) =
    (iterateFrobeniusEquiv R p (m + n)) ((iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x))

Tactic:
rw [RingEquiv.apply_symm_apply, add_comm,
    iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_apply, RingEquiv.apply_symm_apply]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f p : R[X]
⊢ (aeval (root f)) p = (mk f) p

Tactic:
rw [aeval_eq_of_algebra, Algebra.algebraMap_self, Polynomial.map_id]

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 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
⊢ (Ideal.span {map (algebraMap K R) (minpoly K g)}).IsRadical

Tactic:
← isRadical_iff_span_singleton

Goal state after:
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
⊢ IsRadical (map (algebraMap K R) (minpoly K g))
Module: Mathlib.Algebra.Lie.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
D D1✝ D2✝ : LieDerivation R L M
a✝ b✝ : L
D1 D2 : LieDerivation R L M
a b : L
⊢ (↑D1 - ↑D2) ⁅a, b⁆ = ⁅a, (↑D1 - ↑D2) b⁆ - ⁅b, (↑D1 - ↑D2) a⁆

Tactic:
simp only [LinearMap.sub_apply, coeFn_coe, apply_lie_eq_sub, lie_sub, sub_sub_sub_comm]

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

Goal state before:
pp: case calc_3
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
⊢ ∑ i ∈ R2N, ∑ j ∈ range (i + 1), ((↑j !)⁻¹ * (↑(i - j)!)⁻¹) • (a ^ j * b ^ (i - j)) =
    ∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)

Tactic:
hR2N,

Goal state after:
case calc_3
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
⊢ ∑ i ∈ range (2 * N + 1), ∑ j ∈ range (i + 1), ((↑j !)⁻¹ * (↑(i - j)!)⁻¹) • (a ^ j * b ^ (i - j)) =
    ∑ ij ∈ range (2 * N + 1) ×ˢ range (2 * N + 1) with ij.1 + ij.2 ≤ 2 * N,
      ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case calc_1
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₂ : ∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₂ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
restrict :
  ∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) =
    ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
x✝³ : ℕ
x✝² : x✝³ ∈ RN
x✝¹ : ℕ
x✝ : x✝¹ ∈ RN
⊢ (↑x✝³!)⁻¹ • a ^ x✝³ * (↑x✝¹!)⁻¹ • b ^ x✝¹ = ((↑x✝³!)⁻¹ * (↑x✝¹!)⁻¹) • (a ^ x✝³ * b ^ x✝¹)

Tactic:
rw [smul_mul_assoc, mul_smul_comm, smul_smul]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
⊢ x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅y, x⁆ ∈ H

Tactic:
rw [Subtype.forall']

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
⊢ x ∈ H.normalizer ↔ ∀ (x_1 : ↥H), ⁅↑x_1, x⁆ ∈ H
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
n : ℕ
b : P
x✝ : map (↑g) (m • (C b * X ^ n)) = (MonoidHom.id M) m • map (↑g) (C b * X ^ n)
⊢ C (m • g b) * X ^ (n + 1) = C (m • ↑g b) * X ^ (n + 1)

Tactic:
coe_fn_coe

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
n : ℕ
b : P
x✝ : map (↑g) (m • (C b * X ^ n)) = (MonoidHom.id M) m • map (↑g) (C b * X ^ n)
⊢ C (m • g b) * X ^ (n + 1) = C (m • g b) * X ^ (n + 1)
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 : ℕ
h : N₁ ≤ N₂
⊢ ucs k N₁ ≤ ucs k N₂

Tactic:
induction k with
  | zero => simpa
  | succ k ih =>
    simp only [ucs_succ]
    gcongr

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
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian R ↥K
hK₂ : K ≠ ⊤
⊢ maxTrivSubmodule R (↥K) (↥L' ⧸ K.toLieSubmodule) ≠ ⊥

Tactic:
←
      LieSubmodule.nontrivial_iff_ne_bot R K

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
K : LieSubalgebra R ↥L'
hK₁ : IsEngelian R ↥K
hK₂ : K ≠ ⊤
⊢ Nontrivial ↥(maxTrivSubmodule R (↥K) (↥L' ⧸ K.toLieSubmodule))
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: M : Type u
inst✝⁷ : Monoid M
G : Type u
inst✝⁶ : Group G
K : Type u_1
F : Type v
inst✝⁵ : Field F
inst✝⁴ : MulSemiringAction M F
inst✝³ : MulSemiringAction G F
m : M
inst✝² : Field K
inst✝¹ : Algebra K F
inst✝ : SMulCommClass M K F
g : M
x : F
hx : x ∈ subfield M F
g' : M
⊢ g' • g • x = g • x

Tactic:
rw [hx, hx]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id (insert a ↑s)
⊢ LinearIndepOn F (⇑(toFun G F)) (insert a ↑s)

Tactic:
rw [linearIndepOn_insert (mt mem_coe.1 has)] at hs

Goal state after:
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
⊢ LinearIndepOn F (⇑(toFun G F)) (insert a ↑s)
Module: Mathlib.FieldTheory.IntermediateField.Algebraic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
⊢ F = E

Tactic:
refine le_antisymm h_le (fun l hl ↦ ?_)
  rwa [← mem_extendScalars (le_refl F), eq_of_le_of_finrank_le''
    ((extendScalars_le_extendScalars_iff (le_refl F) h_le).2 h_le) h_finrank, mem_extendScalars]

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 : ∀ (x : E), IsIntegral F x ∧ (map (algebraMap F E) (minpoly F x)).Splits
f : F ≃+* M
g : E ≃+* N
hcomp : (algebraMap M N).comp ↑f = (↑g).comp (algebraMap F E)
this : Normal F E
x : N
⊢ (map (algebraMap M N) (minpoly M (g (g.symm x)))).Splits

Tactic:
← minpoly.map_eq_of_equiv_equiv hcomp,

Goal state after:
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 : ∀ (x : E), IsIntegral F x ∧ (map (algebraMap F E) (minpoly F x)).Splits
f : F ≃+* M
g : E ≃+* N
hcomp : (algebraMap M N).comp ↑f = (↑g).comp (algebraMap F E)
this : Normal F E
x : N
⊢ (map (algebraMap M N) (map (↑f) (minpoly F (g.symm x)))).Splits
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : EssFiniteType F E
inst✝ : Algebra.IsAlgebraic F E
s : Finset E
hs : adjoin F ↑s = ⊤
⊢ FiniteType F E

Tactic:
use s

Goal state after:
case h
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : EssFiniteType F E
inst✝ : Algebra.IsAlgebraic F E
s : Finset E
hs : adjoin F ↑s = ⊤
⊢ Algebra.adjoin F ↑s = ⊤
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
p : K[X]
F : IntermediateField K L
⊢ (Polynomial.map (algebraMap K ↥F) p).Splits → (Algebra.adjoin K (p.rootSet ↥F) = ⊤ ↔ F = adjoin K (p.rootSet L))

Tactic:
rw [← toSubalgebra_injective.eq_iff,
      adjoin_toSubalgebra_of_isAlgebraic fun x ↦ isAlgebraic_of_mem_rootSet]

Goal state after:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
⊢ (Polynomial.map (algebraMap K ↥F) p).Splits →
    (Algebra.adjoin K (p.rootSet ↥F) = ⊤ ↔ F.toSubalgebra = Algebra.adjoin K (p.rootSet L))
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : A
hp : IsIdempotentElem p
⊢ spectrum 𝕜 p ⊆ {0, 1}

Tactic:
nontriviality A
  apply Set.image_subset_iff.mp (spectrum.subset_polynomial_aeval p (X ^ 2 - X)) |>.trans
  refine fun a ha => eq_zero_or_one_of_sq_eq_self ?_
  simpa [pow_two p, hp.eq, sub_eq_zero] using ha

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

Goal state before:
pp: case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) → f ∣ derivative f * g

Tactic:
IsAlgClosed.dvd_iff_roots_le_roots hf0 hdg,

Goal state after:
case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : CharZero K
f g : K[X]
hf0 : f ≠ 0
hg0 : ¬g = 0
hdf0 : ¬derivative f = 0
hdg : derivative f * g ≠ 0
⊢ (∀ (x : K), f.IsRoot x → g.IsRoot x) → f.roots ≤ (derivative f * g).roots
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: case refine_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
hp : Nat.Prime (finrank F E)
K : IntermediateField F E
⊢ K = ⊥ ∨ K = ⊤

Tactic:
simpa [← toSubalgebra_strictMono.apply_eq_bot_iff, ← toSubalgebra_strictMono.apply_eq_top_iff]
      using (Subalgebra.isSimpleOrder_of_finrank_prime _ _ hp).eq_bot_or_eq_top K.toSubalgebra

Goal state after: