mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
n : ℕ
ih : ∀ (y : ↥N), ↑(((toEnd R L ↥N) x ^ n) y) = ((toEnd R L M) x ^ n) ↑y
y : ↥N
⊢ ↑(((toEnd R L ↥N) x ^ (n + 1)) y) = ((toEnd R L M) x ^ (n + 1)) ↑y

Tactic:
simp only [pow_succ', Module.End.mul_apply, ih, LieSubmodule.coe_toEnd]

Goal state after:
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
p : Submodule R L
⊢ (lieSpan R L ↑p).toSubmodule = p ↔ ∃ K, K.toSubmodule = p

Tactic:
rw [p.exists_lieSubalgebra_coe_eq_iff]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (lieSpan R L ↑p).toSubmodule = p ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case smul
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x : L
t : R
u : L
hx✝ : u ∈ lieSpan R L s
hu : ⟨u, hx✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)
⊢ ⟨t • u, ⋯⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)

Tactic:
revert hu

Goal state after:
case smul
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x : L
t : R
u : L
hx✝ : u ∈ lieSpan R L s
⊢ ⟨u, hx✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s) →
    ⟨t • u, ⋯⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case a.smul
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
t : R
u : L
hx✝ : u ∈ lieSpan R L (range (Subtype.val ∘ f))
hu : u ∈ map K.incl (lieSpan R (↥K) (range f))
⊢ t • u ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
revert hu

Goal state after:
case a.smul
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
t : R
u : L
hx✝ : u ∈ lieSpan R L (range (Subtype.val ∘ f))
⊢ u ∈ map K.incl (lieSpan R (↥K) (range f)) → t • u ∈ map K.incl (lieSpan R (↥K) (range f))
Module: Mathlib.Algebra.Lie.IdealOperations

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
⊢ map N.incl (comap N.incl N') = N ⊓ N'

Tactic:
by
  rw [← toSubmodule_inj]
  exact (N : Submodule R M).map_comap_subtype N'

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

Goal state before:
pp: case a
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
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
aux : ∀ (y : L), ∀ m' ∈ Submodule.span R s, ⁅y, m'⁆ ∈ Submodule.span R s
⊢ ⁅I, N⁆ ≤
    let __src := Submodule.span R s;
    { toSubmodule := __src, lie_mem := ⋯ }

Tactic:
lieIdeal_oper_eq_span,

Goal state after:
case a
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
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
aux : ∀ (y : L), ∀ m' ∈ Submodule.span R s, ⁅y, m'⁆ ∈ Submodule.span R s
⊢ lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤
    let __src := Submodule.span R s;
    { toSubmodule := __src, lie_mem := ⋯ }
Module: Mathlib.Algebra.Lie.IdealOperations

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
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N⁆ ≤ N' ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'

Tactic:
lieIdeal_oper_eq_span,

Goal state after:
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
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ N' ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, J⁆ ≤ ⁅J, I⁆

Tactic:
lieIdeal_oper_eq_span,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ ⁅J, I⁆
Module: Mathlib.Algebra.Lie.IdealOperations

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
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N⁆ ≤ N

Tactic:
lieIdeal_oper_eq_span,

Goal state after:
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
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ N
Module: Mathlib.Algebra.Lie.IdealOperations

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
inst✝ : LieAlgebra R L
⊢ ⁅⊥, N⁆ ≤ ⊥

Tactic:
lieIdeal_oper_eq_span,

Goal state after:
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
inst✝ : LieAlgebra R L
⊢ lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ ⊥
Module: Mathlib.Algebra.Lie.IdealOperations

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
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N⁆ = ⊥ ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0

Tactic:
lieIdeal_oper_eq_span,

Goal state after:
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
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} = ⊥ ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0
Module: Mathlib.Algebra.Lie.IdealOperations

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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : m ∈ ⁅I, N⁆
⊢ m ∈ ⁅J, N'⁆

Tactic:
lieIdeal_oper_eq_span,

Goal state after:
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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : m ∈ lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
⊢ m ∈ ⁅J, N'⁆
Module: Mathlib.Algebra.Lie.IdealOperations

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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : ∀ (N_1 : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N_1 → m ∈ N_1
⊢ m ∈ ⁅J, N'⁆

Tactic:
lieIdeal_oper_eq_span,

Goal state after:
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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : ∀ (N_1 : LieSubmodule R L M), {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑N_1 → m ∈ N_1
⊢ m ∈ lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
Module: Mathlib.Algebra.Lie.IdealOperations

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
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
⊢ ⁅I, N ⊔ N'⁆ ≤ ⁅I, N⁆ ⊔ ⁅I, N'⁆

Tactic:
lieIdeal_oper_eq_span,

Goal state after:
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
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
⊢ lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ ⁅I, N⁆ ⊔ ⁅I, N'⁆
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: case refine_2.mem
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x y : L
hy : y ∈ lieSpan R L s
w : L
hw : w ∈ s
⊢ ⁅⟨w, ⋯⟩, ⟨y, hy⟩⁆ = 0

Tactic:
| mem w hw =>

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

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 : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ ⁅I, N⁆ ≤ ⊥

Tactic:
lieIdeal_oper_eq_span,

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
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
⊢ lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ ⊥
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
⊢ (if hx : IsIntegral A x then ⋯.min (fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx else 0).Monic

Tactic:
rw [dif_pos hx]

Goal state after:
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
Module: Mathlib.Algebra.Lie.IdealOperations

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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
⊢ ⁅I ⊔ J, N⁆ ≤ ⁅I, N⁆ ⊔ ⁅J, N⁆

Tactic:
lieIdeal_oper_eq_span,

Goal state after:
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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
⊢ lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ≤ ⁅I, N⁆ ⊔ ⁅J, N⁆
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✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : (Polynomial.aeval x) p = 0
⊢ p * C p.leadingCoeff⁻¹ = minpoly A x

Tactic:
have : p.leadingCoeff ≠ 0 := leadingCoeff_ne_zero.mpr hp1.ne_zero

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : (Polynomial.aeval x) p = 0
this : p.leadingCoeff ≠ 0
⊢ p * C p.leadingCoeff⁻¹ = minpoly A x
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✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
⊢ IsUnit f ∨ g = 1

Tactic:
← hg.isUnit_iff

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
⊢ IsUnit f ∨ IsUnit g
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
pb : PowerBasis R S
y : S
a✝ : Nontrivial S
⊢ ∃ f, y = (aeval pb.gen) f

Tactic:
obtain ⟨f, _, hf⟩ := exists_eq_aeval pb y

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
pb : PowerBasis R S
y : S
a✝ : Nontrivial S
f : R[X]
left✝ : f.natDegree < pb.dim
hf : y = (aeval pb.gen) f
⊢ ∃ f, y = (aeval pb.gen) 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
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : p.natDegree < pb.dim
i : Fin pb.dim
root : ∑ i ∈ Finset.range pb.dim, p.coeff i • pb.gen ^ i = 0
⊢ (monomial ↑i) (p.coeff ↑i) = 0

Tactic:
Finset.sum_range,

Goal state after:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
p : A[X]
ne_zero : p ≠ 0
hlt : p.natDegree < pb.dim
i : Fin pb.dim
root : ∑ i, p.coeff ↑i • pb.gen ^ ↑i = 0
⊢ (monomial ↑i) (p.coeff ↑i) = 0
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
f : A[X]
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) f) = (aeval y) f

Tactic:
by
  cases subsingleton_or_nontrivial A
  · rw [(Subsingleton.elim _ _ : f = 0), aeval_zero, map_zero, aeval_zero]
  rw [← aeval_modByMonic_eq_self_of_root (minpoly.aeval _ _), ← aeval_modByMonic_eq_self_of_root hy]
  by_cases hf : f %ₘ minpoly A pb.gen = 0
  · simp only [hf, map_zero]
  have : (f %ₘ minpoly A pb.gen).natDegree < pb.dim := by
    rw [← pb.natDegree_minpoly]
    apply natDegree_lt_natDegree hf
    exact degree_modByMonic_lt _ (minpoly.monic pb.isIntegral_gen)
  rw [aeval_eq_sum_range' this, aeval_eq_sum_range' this, map_sum]
  refine Finset.sum_congr rfl fun i (hi : i ∈ Finset.range pb.dim) => ?_
  rw [Finset.mem_range] at hi
  rw [map_smul]
  congr
  rw [← Fin.val_mk hi, ← pb.basis_eq_pow ⟨i, hi⟩, Basis.constr_basis]

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

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

Tactic:
simp only [hp, coe_eval₂Hom, Ideal.Quotient.lift_mk, eval₂_mul, map_mul, eval₂_X]

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

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

Tactic:
intro r
    rw [Ideal.Quotient.lift_mk, eval₂Hom_C, RingHom.comp_apply, eval₂_C, Ideal.Quotient.lift_mk,
      RingHom.comp_apply]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
⊢ (X ^ n - C ↑u).Separable

Tactic:
by
  nontriviality R
  rcases n.eq_zero_or_pos with (rfl | hpos)
  · simp at hn
  apply (separable_def' (X ^ n - C (u : R))).2
  obtain ⟨n', hn'⟩ := hn.exists_left_inv
  refine ⟨-C ↑u⁻¹, C (↑u⁻¹ : R) * C n' * X, ?_⟩
  rw [derivative_sub, derivative_C, sub_zero, derivative_pow X n, derivative_X, mul_one]
  calc
    -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (↑n * X ^ (n - 1)) =
        C (↑u⁻¹ * ↑u) - C ↑u⁻¹ * X ^ n + C ↑u⁻¹ * C (n' * ↑n) * (X * X ^ (n - 1)) := by
      simp only [C.map_mul, C_eq_natCast]
      ring
    _ = 1 := by
      simp only [Units.inv_mul, hn', C.map_one, mul_one, ← pow_succ',
        Nat.sub_add_cancel (show 1 ≤ n from hpos), sub_add_cancel]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
ι : Type u_1
f : ι → F
s : Finset ι
H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
⊢ (∏ i ∈ s, (X - C (f i))).Separable

Tactic:
by
    rw [← prod_attach]
    exact
      separable_prod'
        (fun x _hx y _hy hxy =>
          @pairwise_coprime_X_sub_C _ _ { x // x ∈ s } (fun x => f x)
            (fun x y hxy => Subtype.ext <| H x.1 x.2 y.1 y.2 hxy) _ _ hxy)
        fun _ _ => separable_X_sub_C

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝¹ : Field F
ι : Type u_1
inst✝ : Fintype ι
f : ι → F
⊢ (∀ (x y : ι), f x = f y → x = y) ↔ Function.Injective f

Tactic:
Function.Injective

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
inst✝¹ : IsDomain R
inst✝ : Free R M
f : M →ₗ[R] M
hf : LinearMap.det f = 0
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
⊢ ⊥ < f.ker

Tactic:
suffices ∃ x, f x = 0 ∧ x ≠ 0 by simpa [bot_lt_iff_ne_bot, ker_eq_bot']

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Free R M
f : M →ₗ[R] M
hf : LinearMap.det f = 0
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
⊢ ∃ x, f x = 0 ∧ x ≠ 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✝ : DecidableEq R
⊢ Finset.image (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots.toFinset ⊆ f.roots.toFinset

Tactic:
by
  rw [Finset.image_toFinset, ← (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne',
    toFinset_subset]
  exact subset_of_le (roots_expand_pow_map_iterateFrobenius_le p n f)

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
H : ((expand R (p ^ n)) (X - C y)).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) (X - C y).roots
⊢ (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}

Tactic:
roots_X_sub_C,

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
H : ((expand R (p ^ n)) (X - C y)).roots = p ^ n • Multiset.map ⇑(iterateFrobeniusEquiv R p n).symm {y}
⊢ (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
Module: Mathlib.Algebra.Lie.AdjointAction.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
⊢ IsNilpotent ((ad R A) a)

Tactic:
rw [LieAlgebra.ad_eq_lmul_left_sub_lmul_right]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)
Module: Mathlib.Algebra.Lie.AdjointAction.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
n : ℕ
hn : (LieAlgebra.ad R L) ↑x ^ n = 0
⊢ IsNilpotent ((LieAlgebra.ad R ↥K) x)

Tactic:
use n

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
L : Type u_3
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
n : ℕ
hn : (LieAlgebra.ad R L) ↑x ^ n = 0
⊢ (LieAlgebra.ad R ↥K) x ^ n = 0
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
⊢ ((ad K (Module.End K V)) a).IsSemisimple

Tactic:
rw [LieAlgebra.ad_eq_lmul_left_sub_lmul_right]

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
⊢ ((LinearMap.mulLeft K - LinearMap.mulRight K) a).IsSemisimple
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
M' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι✝ : Type u_4
inst✝³ : DecidableEq ι✝
inst✝² : Fintype ι✝
e : Basis ι✝ R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit (LinearMap.det f)
hR : Nontrivial R
ι : Type u_2
b : Basis ι R M
this✝¹ : Finite ι
this✝ : Fintype ι
this : DecidableEq ι
⊢ IsUnit ((toMatrix b b) f).det

Tactic:
by rwa [det_toMatrix b]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case ih
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
p✝ : R[X]
⊢ g ∣ p✝ - g * (p✝ /ₘ g) - p✝

Tactic:
sub_sub_cancel_left,

Goal state after:
case ih
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
p✝ : R[X]
⊢ g ∣ -(g * (p✝ /ₘ g))
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
hn : IsNilpotent f
hs : f.IsFinitelySemisimple
⊢ f = 0

Tactic:
have (p) (hp₁ : p ∈ f.invtSubmodule) (hp₂ : Module.Finite R p) : f.restrict hp₁ = 0 := by
    specialize hs p hp₁ hp₂
    replace hn : IsNilpotent (f.restrict hp₁) := isNilpotent.restrict hp₁ hn
    exact eq_zero_of_isNilpotent_isSemisimple hn hs

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
hn : IsNilpotent f
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
⊢ f = 0
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
⊢ exp a • m = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m

Tactic:
by
  rcases le_or_gt (nilpotencyClass a) k with h₀ | h₀
  · simp_rw [exp_eq_sum (pow_eq_zero_of_le h₀ (pow_nilpotencyClass hn)), sum_smul, smul_assoc]
  rw [exp, sum_smul, ← sum_range_add_sum_Ico _ (Nat.le_of_succ_le h₀)]
  suffices ∑ i ∈ Ico k (nilpotencyClass a), ((i.factorial : ℚ)⁻¹ • (a ^ i)) • m = 0 by
    simp_rw [this, add_zero, smul_assoc]
  refine sum_eq_zero fun r h₂ ↦ ?_
  rw [smul_assoc, ← pow_sub_mul_pow a (mem_Ico.1 h₂).1, mul_smul, h, smul_zero, smul_zero]

Goal state after: