mathlib-initiative/mathlib-tactics huggingface dataset:
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:
;

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

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

Goal state after:
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
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inl
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Subsingleton A
⊢ (Algebra.leftMulMatrix pb.basis) pb.gen =
    Matrix.of fun i j ↦ if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0

pp: case inr
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
⊢ (Algebra.leftMulMatrix pb.basis) pb.gen =
    Matrix.of fun i j ↦ if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0

Tactic:
;

Goal state after:
case inl
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Subsingleton A
⊢ (Algebra.leftMulMatrix pb.basis) pb.gen =
    Matrix.of fun i j ↦ if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0

case inr
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
⊢ (Algebra.leftMulMatrix pb.basis) pb.gen =
    Matrix.of fun i j ↦ if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0
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)
⊢ ∀ (a : R ⧸ I),
    (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 a)) =
      C a

Tactic:
intro r

Goal state after:
case C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
r : R ⧸ I
⊢ (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 r)) =
    C r
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
⊢ LinearIndependent K fun i ↦ x ^ ↑i

pp: case neg
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent K fun i ↦ x ^ ↑i

Tactic:
;

Goal state after:
case pos
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
⊢ LinearIndependent K fun i ↦ x ^ ↑i

case neg
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent K fun i ↦ x ^ ↑i
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

Goal state after:
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))
      ((Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
        ((Ideal.Quotient.mk (Ideal.map C I)) (C 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
h : ¬∃ s, Nonempty (Basis (↥s) R S)
x : S
⊢ (if H : ∃ s, Nonempty (Basis (↥s) R S) then detAux (Trunc.mk ⋯.some) else 1) ((lmul R S) x) = 1

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
h : ¬∃ s, Nonempty (Basis (↥s) R S)
x : S
⊢ (if H : ∃ s, Nonempty (Basis (↥s) R S) then detAux (Trunc.mk ⋯.some) else 1) ((lmul R S) x) = 1
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 ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ ((toMatrix b b) ((lmul R S) s)).det = ((toMatrix b b) (mulLeft R s)).det

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ ((toMatrix b b) ((lmul R S) s)).det = ((toMatrix b b) (mulLeft R s)).det
Module: Mathlib.FieldTheory.KummerPolynomial

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

Tactic:
rw [map_zero, sub_zero] at H

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
hn : n ≠ 1
H : Irreducible (X ^ n)
⊢ False
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ x ^ 2 ∣ x ^ n

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ x ^ 2 ∣ x ^ n
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case refine_1.inl
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ 0
⊢ (0 = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree 0

pp: case refine_1.inr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
hr : r ≠ 0
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

Tactic:
· exact .inl (by simpa using h)

Goal state after:
case refine_1.inr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
hr : r ≠ 0
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
z w : R
h0 : z ≠ 0 ∧ z * w ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
⊢ z * w ≠ 0

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
z w : R
h0 : z ≠ 0 ∧ z * w ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
⊢ z * w ≠ 0
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative (f * g))
⊢ f.Separable

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative (f * g))
⊢ f.Separable
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative (f * g))
⊢ IsCoprime f g

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f (derivative (f * g))
⊢ IsCoprime f g
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable
h2 : (f a).Separable ∧ ∀ x ∈ s, (f x).Separable
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ x ∈ s, a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ x ∈ s, x ≠ a → IsCoprime (f x) (f a)) ∧ ∀ x ∈ s, ∀ x_2 ∈ s, x ≠ x_2 → IsCoprime (f x) (f x_2)
⊢ (∏ x ∈ insert a s, f x).Separable

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable
h2 : (f a).Separable ∧ ∀ x ∈ s, (f x).Separable
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ x ∈ s, a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ x ∈ s, x ≠ a → IsCoprime (f x) (f a)) ∧ ∀ x ∈ s, ∀ x_2 ∈ s, x ≠ x_2 → IsCoprime (f x) (f x_2)
⊢ (∏ x ∈ insert a s, f x).Separable
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
a✝ : Nontrivial A
e : n ≃ m := indexEquivOfInv hMM' hM'M
⊢ (M * N).det = (N * M).det

Tactic:
rw [← det_submatrix_equiv_self e, ← submatrix_mul_equiv _ _ _ (Equiv.refl n) _, det_comm,
    submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: M : Type u_1
p q : ℕ
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
inst✝ : PerfectRing M q
⊢ Bijective fun x ↦ (x ^ p) ^ q

Tactic:
;

Goal state after:
M : Type u_1
p q : ℕ
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
inst✝ : PerfectRing M q
⊢ Bijective fun x ↦ (x ^ p) ^ q
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ ⇑(iterateFrobeniusEquiv R p n) = (⇑((RingAut.toPerm R) (frobeniusEquiv R p)))^[n]

Tactic:
;

Goal state after:
R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ ⇑(iterateFrobeniusEquiv R p n) = (⇑((RingAut.toPerm R) (frobeniusEquiv R p)))^[n]
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ (frobeniusEquiv R p ^ n).symm = (frobeniusEquiv R p).symm ^ n

Tactic:
;

Goal state after:
R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ (frobeniusEquiv R p ^ n).symm = (frobeniusEquiv R p).symm ^ n
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:
;

Goal state after:
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✝
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:
;

Goal state after:
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✝
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case h
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
⊢ Function.Commute ⇑(frobeniusEquiv S p) ⇑(frobeniusEquiv S p).symm

Tactic:
;

Goal state after:
case h
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
⊢ Function.Commute ⇑(frobeniusEquiv S p) ⇑(frobeniusEquiv S p).symm
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case h
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
⊢ Function.Commute ⇑(frobeniusEquiv R p) ⇑(frobeniusEquiv R p).symm

Tactic:
;

Goal state after:
case h
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
⊢ Function.Commute ⇑(frobeniusEquiv R p) ⇑(frobeniusEquiv R p).symm
Module: Mathlib.FieldTheory.Perfect

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

Tactic:
;

Goal state after:
case prime.inr
K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
hp : Nat.Prime p
hchar✝ : CharP K p
g : K[X]
hf : Irreducible ((expand K p) g)
⊢ False
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]
⊢ Irreducible ((expand K p) g) → False

Tactic:
;

Goal state after:
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]
⊢ Irreducible ((expand K p) g) → False
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:
;

Goal state after:
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
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
r : R
⊢ p ^ n * (filter (fun x ↦ r ^ p ^ n = x) f.roots).card =
    p ^ n * (filter (fun a ↦ r = (iterateFrobeniusEquiv R p n).symm a) f.roots).card

Tactic:
;

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
r : R
⊢ p ^ n * (filter (fun x ↦ r ^ p ^ n = x) f.roots).card =
    p ^ n * (filter (fun a ↦ r = (iterateFrobeniusEquiv R p n).symm a) f.roots).card
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case e_a.e_p
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
r : R
⊢ (fun x ↦ r ^ p ^ n = x) = fun a ↦ r = (iterateFrobeniusEquiv R p n).symm a

Tactic:
;

Goal state after:
case e_a.e_p
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
r : R
⊢ (fun x ↦ r ^ p ^ n = x) = fun a ↦ r = (iterateFrobeniusEquiv R p n).symm a
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
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
⊢ ((toMatrix B B) (pi fun i ↦ f i ∘ₗ proj i)).det = ∏ i, LinearMap.det (f i)

Tactic:
← LinearMap.det_toMatrix b

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
⊢ ((toMatrix B B) (pi fun i ↦ f i ∘ₗ proj i)).det = ∏ x, ((toMatrix b b) (f x)).det
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
⊢ annIdeal 𝕜 f = Module.annihilator 𝕜[X] (Module.AEval' f)

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
⊢ annIdeal 𝕜 f = Module.annihilator 𝕜[X] (Module.AEval' f)
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
x✝ : 𝕜[X]
⊢ (∀ (x : M), ((aeval f) x✝) x = 0 x) ↔ ∀ (m : Module.AEval' f), x✝ • m = 0

Tactic:
;

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
f : Module.End 𝕜 M
x✝ : 𝕜[X]
⊢ (∀ (x : M), ((aeval f) x✝) x = 0 x) ↔ ∀ (m : Module.AEval' f), x✝ • m = 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommSemiring S
inst✝² : Semiring T
inst✝¹ : Algebra S R
inst✝ : Algebra S T
p : R[X]
f g : AdjoinRoot p →ₐ[S] T
hAlg : f.comp (ofAlgHom S p) = g.comp (ofAlgHom S p)
hRoot : f (root p) = g (root p)
⊢ ↑f = ↑g

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommSemiring S
inst✝² : Semiring T
inst✝¹ : Algebra S R
inst✝ : Algebra S T
p : R[X]
f g : AdjoinRoot p →ₐ[S] T
hAlg : f.comp (ofAlgHom S p) = g.comp (ofAlgHom S p)
hRoot : f (root p) = g (root p)
⊢ ↑f = ↑g
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 R (AdjoinRoot f)) a = (of f) ((algebraMap R S) a)

Tactic:
rw [IsScalarTower.algebraMap_apply R S]

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

Tactic:
;

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)
x✝¹ : Module.End K V
x✝ : V
⊢ ((LinearMap.mulRight K a) x✝¹) x✝ = (((Algebra.lsmul K K (Module.End K V)) (MulOpposite.op a)) x✝¹) x✝
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
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 : q ∣ Polynomial.map f p
⊢ eval₂ ((of q).comp f) (root q) p = 0

Tactic:
by simpa [← Polynomial.eval₂_map, ← algebraMap_eq, ← aeval_def]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
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✝ : S
⊢ ((↑f.toRingEquiv.symm).comp ↑f) x✝ = (RingHom.id S) x✝

Tactic:
;

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
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✝ : S
⊢ ((↑f.toRingEquiv.symm).comp ↑f) x✝ = (RingHom.id S) x✝
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ b'.toMatrix (⇑f ∘ ⇑b) = (LinearMap.toMatrix b b') f

Tactic:
;

Goal state after:
M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ b'.toMatrix (⇑f ∘ ⇑b) = (LinearMap.toMatrix b b') f
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✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ≥0
⊢ ↑q = (of f) ↑q

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ≥0
⊢ ↑q = (of f) ↑q
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b b' b'' : Basis ι A M
x✝ : ι
⊢ b'' x✝ = (⇑↑(b'.equiv b'' (Equiv.refl ι)) ∘ ⇑b') x✝

Tactic:
;

Goal state after:
M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b b' b'' : Basis ι A M
x✝ : ι
⊢ b'' x✝ = (⇑↑(b'.equiv b'' (Equiv.refl ι)) ∘ ⇑b') x✝
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✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ
⊢ ↑q = (of f) ↑q

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ
⊢ ↑q = (of f) ↑q