mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid 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)
l : ℕ
hl : n ≤ l
m : ℕ
h : m < l
⊢ (f ^ l).range ≤ (f ^ m).range

Tactic:
· exact f.iterateRange.monotone h.le

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

Goal state before:
pp: R : Type u_1
P : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup P
inst✝ : Module R P
S : Submodule R P
⊢ IsArtinian R P ↔ IsArtinian R ↥S ∧ IsArtinian R (P ⧸ S)

Tactic:
refine ⟨fun h ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ ?_⟩
  apply isArtinian_of_range_eq_ker S.subtype S.mkQ
  rw [Submodule.ker_mkQ, Submodule.range_subtype]

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hp : 0 < p
⊢ IsZero ((Y.E₂SpectralSequence.page r ⋯).X (p, q))

Tactic:
by
  apply isZero_spectralSequence_page_X_of_isZero_H' _ _ _ hr
  apply Y.isZero₂_of_isThirdQuadrant
  simp
  lia

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

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
⊢ 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = 0

Tactic:
convert (commute_lmul_lmul_sq (a + b)).lie_eq

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b : A
⊢ 2 • ⁅L a, L (a * b)⁆ + 2 • ⁅L b, L (b * a)⁆ + ⁅L b, L (a * a)⁆ + ⁅L a, L (b * b)⁆ = ⁅L (a + b), L ((a + b) * (a + b))⁆
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
⊢ ∀ {x y : L₂}, x ∈ (↑f).range.carrier → y ∈ (↑f).range.carrier → ⁅x, y⁆ ∈ (↑f).range.carrier

Tactic:
rintro - - ⟨x, rfl⟩ ⟨y, rfl⟩
        exact ⟨⁅x, y⁆, f.map_lie x y⟩

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

Goal state before:
pp: case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x : L
hx : x ∈ K
⊢ ⟨x, hx⟩ ∈ comap K.incl (lieSpan R L (range (Subtype.val ∘ f))) → ⟨x, hx⟩ ∈ lieSpan R (↥K) (range f)

Tactic:
hx'

Goal state after:
case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x : L
hx : x ∈ K
hx' : ⟨x, hx⟩ ∈ comap K.incl (lieSpan R L (range (Subtype.val ∘ f)))
⊢ ⟨x, hx⟩ ∈ lieSpan R (↥K) (range f)
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 : LieSubmodule R L M
⊢ ↑N = ⊤ ↔ N = ⊤

Tactic:
rw [← toSubmodule_inj, top_toSubmodule]

Goal state after:
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 : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier
⊢ { toSubmodule := N, lie_mem := h } = ⊤ ↔ N = ⊤

Tactic:
rw [← toSubmodule_inj, top_toSubmodule]

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

Goal state before:
pp: case insert
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
S : Set (LieSubmodule R L M)
x : L
q : Submodule R M
t : Finset (Submodule R M)
hqt : q ∉ t
ih : ∀ {m : M}, ↑t ⊆ {x | ∃ p ∈ S, ↑p = x} → m ∈ ⨆ i ∈ t, i → ⁅x, m⁆ ∈ sSup {x | ∃ p ∈ S, ↑p = x}
hs : ↑(insert q t) ⊆ {x | ∃ p ∈ S, ↑p = x}
m' : M
hm' : m' ∈ q
u : M
hu : u ∈ ⨆ x ∈ t, x
hsm : m' + u ∈ q ⊔ ⨆ x ∈ t, x
⊢ ⁅x, m'⁆ ∈ sSup {x | ∃ p ∈ S, ↑p = x}

Tactic:
obtain ⟨p, hp, rfl⟩ : ∃ p ∈ S, ↑p = q := hs (Finset.mem_insert_self q t)

Goal state after:
case insert
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
S : Set (LieSubmodule R L M)
x : L
t : Finset (Submodule R M)
ih : ∀ {m : M}, ↑t ⊆ {x | ∃ p ∈ S, ↑p = x} → m ∈ ⨆ i ∈ t, i → ⁅x, m⁆ ∈ sSup {x | ∃ p ∈ S, ↑p = x}
m' u : M
hu : u ∈ ⨆ x ∈ t, x
p : LieSubmodule R L M
hp : p ∈ S
hqt : ↑p ∉ t
hs : ↑(insert (↑p) t) ⊆ {x | ∃ p ∈ S, ↑p = x}
hm' : m' ∈ ↑p
hsm : m' + u ∈ ↑p ⊔ ⨆ x ∈ t, x
⊢ ⁅x, m'⁆ ∈ sSup {x | ∃ p ∈ S, ↑p = x}
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case h.left
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieRing L'
inst✝⁶ : LieAlgebra R L'
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
x : L
m' : M'
m : M
hm : m ∈ ↑↑N
hfm : ↑f m = m'
⊢ ⁅x, m⁆ ∈ ↑↑N

Tactic:
apply N.lie_mem hm

Goal state after:
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
hx : IsIntegral A x
⊢ (⋯.min (fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).Monic

Tactic:
exact (degree_lt_wf.min_mem _ hx).1

Goal state after:
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
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ False

Tactic:
refine (one_ne_zero : (1 : B) ≠ 0) ?_

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ 1 = 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
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ = x
⊢ ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)

Tactic:
let fy₁ : ↥(map f I₁) := ⟨f y₁, mem_map hy₁⟩

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 y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ = x
fy₁ : ↥(map f I₁) := ⟨f y₁, ⋯⟩
⊢ ⁅↑⟨y₁, hy₁⟩, ↑⟨y₂, hy₂⟩⁆ ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = ∑ x, (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x

Tactic:
Fintype.sum_eq_single (⟨(k : ℕ) + 1, lt_of_le_of_ne k.2 h⟩ : Fin pb.dim),

Goal state after:
case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ pb.gen ^ (↑k + 1) = (if ↑⟨↑k + 1, ⋯⟩ = ↑k + 1 then 1 else 0) • pb.gen ^ ↑⟨↑k + 1, ⋯⟩

case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ ∀ (x : Fin pb.dim), x ≠ ⟨↑k + 1, ⋯⟩ → (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ I.polynomialQuotientEquivQuotientPolynomial.symm
      (I.polynomialQuotientEquivQuotientPolynomial (Polynomial.map (Quotient.mk I) f)) =
    I.polynomialQuotientEquivQuotientPolynomial.symm ((Quotient.mk (map C I)) f)

Tactic:
RingEquiv.symm_apply_apply,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ Polynomial.map (Quotient.mk I) f = I.polynomialQuotientEquivQuotientPolynomial.symm ((Quotient.mk (map C I)) f)
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ((Quotient.mk I).comp C) y ∈ ((Quotient.mk I).comp C).range
hx : C ⟨((Quotient.mk I).comp C) y, hx'⟩ ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
⊢ C y ∈ I

Tactic:
suffices C (i y) ∈ I.map (Polynomial.mapRingHom i) by
    obtain ⟨f, hf⟩ := mem_image_of_mem_map_of_surjective (Polynomial.mapRingHom i)
      (Polynomial.map_surjective _ (RingHom.rangeRestrict_surjective ((Quotient.mk I).comp C))) this
    refine sub_add_cancel (C y) f ▸ I.add_mem (hi' ?_ : C y - f ∈ I) hf.1
    rw [RingHom.mem_ker, map_sub, hf.2, sub_eq_zero, coe_mapRingHom, map_C]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ((Quotient.mk I).comp C) y ∈ ((Quotient.mk I).comp C).range
hx : C ⟨((Quotient.mk I).comp C) y, hx'⟩ ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
⊢ C (i y) ∈ map (mapRingHom i) I
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
K : Type u_6
inst✝⁴ : Field K
inst✝³ : Algebra A S
S' : Type u_7
inst✝² : Ring S'
inst✝¹ : Algebra A S'
inst✝ : IsDomain B
pb : PowerBasis A S
x : B
⊢ (aeval x) (minpoly A pb.gen) = 0 ↔ (Equiv.refl B) x ∈ (minpoly A pb.gen).aroots B

Tactic:
rw [Equiv.refl_apply, mem_roots_iff_aeval_eq_zero]
    · simp
    · exact map_monic_ne_zero (minpoly.monic pb.isIntegral_gen)

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (minpoly K x).natDegree → K
i : Fin (minpoly K x).natDegree
hg : (aeval x) (∑ x_1, (monomial ↑x_1) (g x_1)) = 0
hn0 : ¬g i = 0
h0 : (∑ x_1, if x_1 = i then g x_1 else 0) = coeff 0 ↑i
⊢ g i = 0

Tactic:
Finset.sum_ite_eq'

Goal state after:
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (minpoly K x).natDegree → K
i : Fin (minpoly K x).natDegree
hg : (aeval x) (∑ x_1, (monomial ↑x_1) (g x_1)) = 0
hn0 : ¬g i = 0
h0 : (if i ∈ Finset.univ then g i else 0) = coeff 0 ↑i
⊢ g i = 0
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⟩⟩

Goal state after:
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)
H' : ¬∃ t, Nonempty (Basis (↥t) A N)
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f
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
n : ℕ
x : R
⊢ (⇑(frobeniusEquiv S p))^[n] (f ((⇑(frobeniusEquiv R p).symm)^[n] x)) =
    (⇑(frobeniusEquiv S p))^[n] ((⇑(frobeniusEquiv S p).symm)^[n] (f x))

Tactic:
simp only [coe_frobeniusEquiv, ← map_iterate_frobenius]
    · rw [← Function.comp_apply (f := (⇑(frobenius R p))^[n]),
          ← Function.comp_apply (f := (⇑(frobenius S p))^[n]),
          ← Function.Commute.comp_iterate, ← Function.Commute.comp_iterate]
      · simp
      all_goals rw [← coe_frobeniusEquiv]; simp [Function.Commute, Function.Semiconj]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ((expand F (p ^ n)) f).Separable
hn : n ≠ 0
⊢ derivative ((expand F (p ^ n)) f) = 0

Tactic:
derivative_expand,

Goal state after:
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ((expand F (p ^ n)) f).Separable
hn : n ≠ 0
⊢ (expand F (p ^ n)) (derivative f) * (↑(p ^ n) * X ^ (p ^ n - 1)) = 0
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✝ : PerfectRing R p
⊢ ((expand R (p ^ n)) f).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots

Tactic:
by
  classical
  refine ext' fun r ↦ ?_
  rw [count_roots, rootMultiplicity_expand_pow, ← count_roots, count_nsmul, count_map,
    count_eq_card_filter_eq]; congr; ext
  exact (iterateFrobeniusEquiv R p n).eq_symm_apply.symm

Goal state after:
Module: Mathlib.FieldTheory.Perfect

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

Tactic:
mul_smul

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
m : ℕ
⊢ m • p ^ n • {(iterateFrobeniusEquiv R p n).symm y} = m • p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
Module: Mathlib.Algebra.Lie.AdjointAction.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : PerfectField K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
hl : Module.End.IsSemisimple (LinearMap.mulLeft K a)
⊢ (Polynomial.aeval (LinearMap.mulRight K a)) (minpoly K a) = 0

Tactic:
have hrw : LinearMap.mulRight K a =
        (Algebra.lsmul (A := (Module.End K V)ᵐᵒᵖ) K K (Module.End K V)) (.op a) := by
      ext; simp [Algebra.lsmul]

Goal state after:
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : PerfectField K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
hl : Module.End.IsSemisimple (LinearMap.mulLeft K a)
hrw : LinearMap.mulRight K a = (Algebra.lsmul K K (Module.End K V)) (MulOpposite.op a)
⊢ (Polynomial.aeval (LinearMap.mulRight K a)) (minpoly K a) = 0
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
g : R[X]
hg : g.Monic
f✝ : AdjoinRoot g
f : R[X]
⊢ g ∣ f - f %ₘ g

Tactic:
rw [modByMonic_eq_sub_mul_div, sub_sub_cancel]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
g : R[X]
hg : g.Monic
f✝ : AdjoinRoot g
f : R[X]
⊢ g ∣ g * (f /ₘ g)
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: case refine_4
M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝⁵ : Module.Finite K R
this✝⁴ : Module.Finite R S
this✝³ : Module.Finite K S
this✝² : IsArtinianRing R
this✝¹ : IsReduced R
this✝ : IsReduced S
φ : S →ₐ[K] End K M :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
this : K[f, g] ≤ φ.range
p : S
ha : φ p ∈ K[f, g]
⊢ (φ.comp (aeval p)) (minpoly K p) = 0

Tactic:
φ.comp_apply,

Goal state after:
case refine_4
M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝⁵ : Module.Finite K R
this✝⁴ : Module.Finite R S
this✝³ : Module.Finite K S
this✝² : IsArtinianRing R
this✝¹ : IsReduced R
this✝ : IsReduced S
φ : S →ₐ[K] End K M :=
  Ideal.Quotient.liftₐ (Ideal.span {map (algebraMap K R) (minpoly K g)})
    (eval₂AlgHom (Ideal.Quotient.liftₐ (Ideal.span {minpoly K f}) (aeval f) ⋯) g ⋯) ⋯
this : K[f, g] ≤ φ.range
p : S
ha : φ p ∈ K[f, g]
⊢ φ ((aeval p) (minpoly K p)) = 0
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: 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})

pp: 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})

Tactic:
· exact coe_lowerCentralSeries_eq_int_aux _ _ L M k

Goal state after:
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.Engel

Goal state before:
pp: case succ
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))
⊢ ↑(⊤.lcs M (i + (l + 1))) ≤ Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))

Tactic:
simp only [LieIdeal.lcs_succ, i.add_succ l, lie_top_eq_of_span_sup_eq_top hxI, sup_le_iff]

Goal state after:
case succ
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))
⊢ Submodule.map ((toEnd R L M) x) ↑(⊤.lcs M (i + l)) ≤
      Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑⁅I, I.lcs M j⁆ ∧
    ↑⁅I, ⊤.lcs M (i + l)⁆ ≤ Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑⁅I, I.lcs M j⁆
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: case succ.refine_1
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))
⊢ Submodule.map ((toEnd R L M) x) (Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))) ≤
    Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑⁅I, I.lcs M j⁆

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:
· rw [Submodule.map_sup, ← Submodule.map_comp, ← Module.End.mul_eq_comp, ← pow_succ', ←
        I.lcs_succ]
      grw [coe_map_toEnd_le]

Goal state after:
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⁆
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
E' : Type u_4
inst✝¹ : Field E'
inst✝ : Algebra F E'
f : E ≃ₐ[F] E'
x : E'
h : IsIntegral F (f.symm x) ∧ (map (algebraMap F E) (minpoly F (f.symm x))).Splits
⊢ IsIntegral F x ∧ (map (algebraMap F E') (minpoly F x)).Splits

Tactic:
← f.apply_symm_apply x,

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
E' : Type u_4
inst✝¹ : Field E'
inst✝ : Algebra F E'
f : E ≃ₐ[F] E'
x : E'
h : IsIntegral F (f.symm x) ∧ (map (algebraMap F E) (minpoly F (f.symm x))).Splits
⊢ IsIntegral F (f (f.symm x)) ∧ (map (algebraMap F E') (minpoly F (f (f.symm x)))).Splits
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
⊢ Polynomial.eval₂ (subfield G F).subtype x (minpoly G F x) = 0

Tactic:
rw [← prodXSubSMul.eval G F x, Polynomial.eval₂_eq_eval_map]
  simp only [minpoly, Polynomial.map_toSubring]

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

Goal state before:
pp: case splits'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ (Polynomial.map ((algebraMap K L).comp (algebraMap F K)) f *
      Polynomial.map ((algebraMap K L).comp (algebraMap F K)) g).Splits

Tactic:
← map_map,

Goal state after:
case splits'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ (Polynomial.map (algebraMap K L) (Polynomial.map (algebraMap F K) f) *
      Polynomial.map ((algebraMap K L).comp (algebraMap F K)) g).Splits