mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Jordan.Basic

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

Tactic:
rw [← lie_skew (L (a * a)), ← lie_skew (L (b * b)), ← lie_skew (L (c * c))]

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (-⁅L b, L (a * a)⁆ + -⁅L a, L (b * b)⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (-⁅L c, L (a * a)⁆ + -⁅L a, L (c * c)⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (-⁅L c, L (b * b)⁆ + -⁅L b, L (c * c)⁆)) =
    0
Module: Mathlib.RingTheory.Polynomial.Quotient

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

Tactic:
eval₂_monomial (C.comp (Quotient.mk I)) X

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
⊢ (C.comp (Quotient.mk I)) (a.coeff n) * X ^ n = 0
Module: Mathlib.LinearAlgebra.Matrix.Dual

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v w : n → R
i✝ : n
⊢ ({ toFun := dotProduct (v + w), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 =
    (({ toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ } +
          { toFun := dotProduct w, map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
        LinearMap.single R (fun i ↦ R) i✝)
      1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Dual

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
t : R
v : n → R
i✝ : n
⊢ ({ toFun := dotProduct (t • v), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 =
    (((RingHom.id R) t • { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ LinearMap.single R (fun i ↦ R) i✝)
      1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Dual

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
⊢ (fun f i ↦ f ((LinearMap.single R (fun a ↦ R) i) 1))
      ((fun v ↦ { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ }) v) =
    v

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Dual

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Dual R (n → R)
i✝ : n
⊢ ((fun v ↦ { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ })
          ((fun f i ↦ f ((LinearMap.single R (fun a ↦ R) i) 1)) f) ∘ₗ
        LinearMap.single R (fun i ↦ R) i✝)
      1 =
    (f ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
H : (pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x = b
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ pb.gen ∈ {pb.gen}

Tactic:
simp

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 ⧸ I)
r : R
⊢ (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)) (C ((Ideal.Quotient.mk I) r))) =
    C ((Ideal.Quotient.mk I) r)

Tactic:
simp

Goal state after:
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 ↔ (aeval x) (map (algebraMap A B) (minpoly A pb.gen)) = 0

Tactic:
simp

Goal state after:
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'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : (aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : (aeval pb'.gen) (minpoly A pb.gen) = 0
f : A[X]
⊢ ((pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁)) ((aeval pb'.gen) f) = (AlgHom.id A S') ((aeval pb'.gen) f)

Tactic:
simp

Goal state after:
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'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : (aeval pb.gen) (minpoly A pb'.gen) = 0
h₂ : (aeval pb'.gen) (minpoly A pb.gen) = 0
f : A[X]
⊢ ((pb'.lift pb.gen h₁).comp (pb.lift pb'.gen h₂)) ((aeval pb.gen) f) = (AlgHom.id A S) ((aeval pb.gen) f)

Tactic:
simp

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 : (lcoeff K ↑i) (∑ x_1, (monomial ↑x_1) (g x_1)) = (lcoeff K ↑i) 0
⊢ g i = 0

Tactic:
simp_rw [map_sum, lcoeff_apply, coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq'] at h0

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.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
⊢ (pb.map e).minpolyGen = pb.minpolyGen

Tactic:
simp

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
r : 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)) (C ((Ideal.Quotient.mk I) r)) =
    (Ideal.Quotient.mk (Ideal.map C I)) (C r)

Tactic:
eval₂_C,

Goal state after:
case C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
r : R
⊢ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯) ((Ideal.Quotient.mk I) r) =
    (Ideal.Quotient.mk (Ideal.map C I)) (C r)
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ ((toMatrix b b) ((lsmul R R S) x)).det = x ^ Fintype.card ι

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
⊢ root (X ^ n - C a) ^ n - (of (X ^ n - C a)) a =
    eval₂ (of (X ^ n - C a)) (root (X ^ n - C a)) (X ^ n) - eval₂ (of (X ^ n - C a)) (root (X ^ n - C a)) (C a)

Tactic:
eval₂_C,

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
a : K
⊢ root (X ^ n - C a) ^ n - (of (X ^ n - C a)) a =
    eval₂ (of (X ^ n - C a)) (root (X ^ n - C a)) (X ^ n) - (of (X ^ n - C a)) a
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
e : root (X - C a) = 0
⊢ (C a).natDegree < (X - C a).natDegree

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
hn : n ≠ 1
H : Irreducible (X ^ n)
⊢ False

Tactic:
exact not_irreducible_pow hn H

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

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ ¬(0 * 0 ∣ 0 → IsUnit 0)

Tactic:
simp

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

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝ : Monoid R
x y : R
hx : Squarefree y
hu : ¬IsUnit x
h : x ^ 0 ∣ y
⊢ x ^ 0 ∣ x

Tactic:
simp

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

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝ : Monoid R
x y : R
hx : Squarefree y
hu : ¬IsUnit x
h : x ^ 1 ∣ y
⊢ x ^ 1 ∣ x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ ¬IsMax 1

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this✝ : ¬IsUnit (X ^ p - C a)
g : K[X]
hg : Irreducible g
hg' : g ∣ X ^ p - C a
h : ¬g.natDegree = p
this : eval₂ (of g) (root g) X ^ p - eval₂ (of g) (root g) (C a) = 0
⊢ (Algebra.norm K) (root g) ^ p = a ^ g.natDegree

Tactic:
eval₂_C,

Goal state after:
K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this✝ : ¬IsUnit (X ^ p - C a)
g : K[X]
hg : Irreducible g
hg' : g ∣ X ^ p - C a
h : ¬g.natDegree = p
this : eval₂ (of g) (root g) X ^ p - (of g) a = 0
⊢ (Algebra.norm K) (root g) ^ p = a ^ g.natDegree
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case empty
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
f : ι → R
hs : (↑∅).Pairwise (IsRelPrime on f)
hs' : ∀ i ∈ ∅, Squarefree (f i)
⊢ Squarefree (∏ i ∈ ∅, f i)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (IsRelPrime on f) → (∀ i ∈ s, Squarefree (f i)) → Squarefree (∏ i ∈ s, f i)
hs : (↑s).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ ↑s, a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
⊢ a ∈ cons a s ha

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
⊢ IsCoprime q q

Tactic:
have : IsCoprime (q * (q * p))
      (q * (derivative q * p + derivative q * p + q * derivative p)) := by
    simp only [← mul_assoc, mul_add]
    dsimp only [Separable] at hp
    convert! hp using 1
    rw [derivative_mul, derivative_mul]
    ring

Goal state after:
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
this : IsCoprime (q * (q * p)) (q * (derivative q * p + derivative q * p + q * derivative p))
⊢ IsCoprime q q
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
s : Finset M
b : Basis (↥s) A M
f : M →ₗ[A] M
this : ∃ s, Nonempty (Basis (↥s) A M)
⊢ LinearMap.det f = ((toMatrix b b) f).det

Tactic:
LinearMap.coe_det,

Goal state after:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
s : Finset M
b : Basis (↥s) A M
f : M →ₗ[A] M
this : ∃ s, Nonempty (Basis (↥s) A M)
⊢ (if H : ∃ s, Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1) f = ((toMatrix b b) f).det
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x✝ : R
⊢ ((frobenius R p).comp ↑(frobeniusEquiv R p).symm) x✝ = (RingHom.id R) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x✝ : R
⊢ ((↑(frobeniusEquiv R p).symm).comp (frobenius R p)) x✝ = (RingHom.id R) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x✝ : R
⊢ (⇑(frobenius R p) ∘ ⇑(frobeniusEquiv R p).symm) x✝ = id x✝

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x✝ : R
⊢ (⇑(frobeniusEquiv R p).symm ∘ ⇑(frobenius R p)) x✝ = id x✝

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case zero
R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
⊢ (⇑(frobeniusEquiv R p).symm)^[0] x ^ p ^ 0 = x

Tactic:
simp

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
n : ℕ
x : R
⊢ f ((⇑(frobenius R p) ∘ ⇑(frobeniusEquiv R p).symm)^[n] x) = (⇑(frobenius S p) ∘ ⇑(frobeniusEquiv S p).symm)^[n] (f x)

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case inj
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
⊢ Injective ⇑(frobeniusEquiv S p)

Tactic:
simp

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]
this : Fact (Nat.Prime p)
⊢ Irreducible ((expand K p) g) → False

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
⊢ LinearMap.det (mulLeft R a) = a

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
⊢ LinearMap.det (mulRight R a) = a

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : (map (algebraMap F K) p).Splits
⊢ Fintype.card ↑↑(p.aroots K).toFinset = p.natDegree

Tactic:
Finset.coe_sort_coe,

Goal state after:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : (map (algebraMap F K) p).Splits
⊢ Fintype.card ↥(p.aroots K).toFinset = p.natDegree
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 =
    ↑(Finset.image (⇑(frobenius R p)) ((expand R p) f).roots.toFinset)

Tactic:
simp

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
f : R[X]
inst✝¹ : DecidableEq R
inst✝ : PerfectRing R p
n : ℕ
⊢ ⇑(iterateFrobeniusEquiv R p n).toEquiv '' ↑((expand R (p ^ n)) f).roots.toFinset =
    ↑(Finset.image (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots.toFinset)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: case neg.h2
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ IsUnit (C (IsPrincipal.generator (annIdeal 𝕜 a)).leadingCoeff⁻¹)

Tactic:
apply Polynomial.isUnit_C.mpr

Goal state after:
case neg.h2
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ IsUnit (IsPrincipal.generator (annIdeal 𝕜 a)).leadingCoeff⁻¹
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
f : F[X]
hf : f ≠ 0
h : (map (algebraMap F K) f).Splits
⊢ Fintype.card ↑↑(f.aroots K).toFinset = f.natDegree ↔ f.Separable

Tactic:
Finset.coe_sort_coe,

Goal state after:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
f : F[X]
hf : f ≠ 0
h : (map (algebraMap F K) f).Splits
⊢ Fintype.card ↥(f.aroots K).toFinset = f.natDegree ↔ f.Separable
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
p : 𝕜[X]
p_monic : p.Monic
hp : (aeval a) p = 0
⊢ p ∈ ⊥

Tactic:
simpa only [annIdealGenerator_eq_zero_iff.mp h] using mem_annIdeal_iff_aeval_eq_zero.mpr hp

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u_1
inst✝² : Field F
K : Type u_2
inst✝¹ : Ring K
inst✝ : Algebra F K
x : F
⊢ (aeval ((algebraMap F K) x)) (X - C x) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case neg
K : Type u_5
m : Type u_6
F : Type u_7
inst✝⁴ : Field K
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : FunLike F (Matrix m m K) (Matrix m m K)
inst✝ : AlgHomClass F K (Matrix m m K) (Matrix m m K)
f : F
x : Matrix m m K
h✝ : IsEmpty m
⊢ (f x).det = x.det

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ f ∣ -f + 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case C
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S[X]
a : R
⊢ (algebraMap S (AdjoinRoot f)) ((algebraMap R S) a) = (of f) ((algebraMap R S) a)

Tactic:
simp

Goal state after:
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)
hrw : LinearMap.mulRight K a = (Algebra.lsmul K K (Module.End K V)) (MulOpposite.op a)
⊢ (Algebra.lsmul K K (Module.End K V)) (MulOpposite.op 0) = 0

Tactic:
MulOpposite.op_zero,

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)
⊢ (Algebra.lsmul K K (Module.End K V)) 0 = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : ϕ.comp (of f) = algebraMap R S
⊢ eval₂ (ϕ.comp (of f)) (ϕ (root f)) f = ϕ.toRingHom 0

Tactic:
← eval₂_root f,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : ϕ.comp (of f) = algebraMap R S
⊢ eval₂ (ϕ.comp (of f)) (ϕ (root f)) f = ϕ.toRingHom (eval₂ (of f) (root f) f)
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
⊢ (liftAlgHom f (Algebra.ofId R S) (ϕ (root f)) ⋯) (root f) = ϕ (root f)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hAlg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
p : R[X]
q : S[X]
r : T[X]
hf : q ∣ Polynomial.map f p
hg : r ∣ Polynomial.map g q
x✝ : R
⊢ (((map g q r hg).comp (map f p q hf)).comp (of p)) x✝ = ((map (g.comp f) p r ⋯).comp (of p)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hRoot
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
p : R[X]
q : S[X]
r : T[X]
hf : q ∣ Polynomial.map f p
hg : r ∣ Polynomial.map g q
⊢ ((map g q r hg).comp (map f p q hf)) (root p) = (map (g.comp f) p r ⋯) (root p)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hAlg
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
x✝ : S
⊢ (((map (↑f) p q ⋯).comp (map (↑f.symm) q p ⋯)).comp (of q)) x✝ = ((RingHom.id (AdjoinRoot q)).comp (of q)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hRoot
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ ((map (↑f) p q ⋯).comp (map (↑f.symm) q p ⋯)) (root q) = (RingHom.id (AdjoinRoot q)) (root q)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hAlg
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
x✝ : R
⊢ (((map (↑f.symm) q p ⋯).comp (map (↑f) p q ⋯)).comp (of p)) x✝ = ((RingHom.id (AdjoinRoot p)).comp (of p)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hRoot
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ ((map (↑f.symm) q p ⋯).comp (map (↑f) p q ⋯)) (root p) = (RingHom.id (AdjoinRoot p)) (root p)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hAlg
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
x✝ : T
⊢ (((mapAlgHom (↑f) p q ⋯).comp (mapAlgHom (↑f.symm) q p ⋯)).comp (ofAlgHom R q)) x✝ =
    ((AlgHom.id R (AdjoinRoot q)).comp (ofAlgHom R q)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case hRoot
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ ((mapAlgHom (↑f) p q ⋯).comp (mapAlgHom (↑f.symm) q p ⋯)) (root q) = (AlgHom.id R (AdjoinRoot q)) (root q)

Tactic:
simp

Goal state after: