mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
hs : IsIntegral R s
p : R[X]
hp : (Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x✝ : Algebra K L := FractionRing.liftAlgebra R L
⊢ (Polynomial.aeval ((algebraMap S L) s)) (map (algebraMap R K) p) = 0

Tactic:
← map_aeval_eq_aeval_map,

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
hs : IsIntegral R s
p : R[X]
hp : (Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x✝ : Algebra K L := FractionRing.liftAlgebra R L
⊢ (algebraMap S L) ((Polynomial.aeval s) p) = 0

case refine_1.h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
hs : IsIntegral R s
p : R[X]
hp : (Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x✝ : Algebra K L := FractionRing.liftAlgebra R L
⊢ (algebraMap K L).comp (algebraMap R K) = (algebraMap S L).comp (algebraMap R S)
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
⊢ Irreducible p ↔ Irreducible (Polynomial.map (algebraMap R K) p)

Tactic:
refine
    ⟨fun hp =>
      irreducible_iff.mpr
        ⟨hp.not_isUnit.imp h.isPrimitive.isUnit_iff_isUnit_map.mpr, fun a b H =>
          or_iff_not_imp_left.mpr fun hₐ => ?_⟩,
      fun hp =>
      h.isPrimitive.irreducible_of_irreducible_map_of_injective (IsFractionRing.injective R K) hp⟩
  obtain ⟨a', ha⟩ := eq_map_mul_C_of_dvd K h (dvd_of_mul_right_eq b H.symm)
  obtain ⟨b', hb⟩ := eq_map_mul_C_of_dvd K h (dvd_of_mul_left_eq a H.symm)
  have : a.leadingCoeff * b.leadingCoeff = 1 := by
    rw [← leadingCoeff_mul, ← H, Monic.leadingCoeff (h.map <| algebraMap R K)]
  rw [← ha, ← hb, mul_comm _ (C b.leadingCoeff), mul_assoc, ← mul_assoc (C a.leadingCoeff), ←
    C_mul, this, C_1, one_mul, ← Polynomial.map_mul] at H
  rw [← hb, ← Polynomial.coe_mapRingHom]
  refine
    IsUnit.mul (IsUnit.map _ (Or.resolve_left (hp.isUnit_or_isUnit ?_) (show ¬IsUnit a' from ?_)))
      (isUnit_iff_exists_inv'.mpr
        (Exists.intro (C a.leadingCoeff) <| by rw [← C_mul, this, C_1]))
  · exact Polynomial.map_injective _ (IsFractionRing.injective R K) H
  · by_contra h_contra
    refine hₐ ?_
    rw [← ha, ← Polynomial.coe_mapRingHom]
    exact
      IsUnit.mul (IsUnit.map _ h_contra)
        (isUnit_iff_exists_inv.mpr
          (Exists.intro (C b.leadingCoeff) <| by rw [← C_mul, this, C_1]))

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: case neg
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hp : p.Separable
hp0 : ¬p = 0
u : k[X]ˣ
hu : (UniqueFactorizationMonoid.factors p).prod * ↑u = p
⊢ p.Splits

Tactic:
← hu

Goal state after:
case neg
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hp : p.Separable
hp0 : ¬p = 0
u : k[X]ˣ
hu : (UniqueFactorizationMonoid.factors p).prod * ↑u = p
⊢ ((UniqueFactorizationMonoid.factors p).prod * ↑u).Splits
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝⁵ : Field k
K : Type v
inst✝⁴ : Field K
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Normal F E
⊢ Normal F ↥(separableClosure F E)

Tactic:
rw [← separableClosure.normalClosure_eq_self]

Goal state after:
k : Type u
inst✝⁵ : Field k
K : Type v
inst✝⁴ : Field K
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Normal F E
⊢ Normal F ↥(IntermediateField.normalClosure F (↥(separableClosure F E)) E)
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F✝ : Type u
E✝ : Type v
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
q : ℕ
inst✝² : ExpChar F✝ q
inst✝¹ : IsPurelyInseparable F✝ E✝
inst✝ : FiniteDimensional F✝ E✝
F E : Type v
⊢ ∀ [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E]
    [FiniteDimensional F E], ∃ n, finrank F E = q ^ n

Tactic:
_

Goal state after:
F✝ : Type u
E✝ : Type v
inst✝⁶ : Field F✝
inst✝⁵ : Field E✝
inst✝⁴ : Algebra F✝ E✝
q : ℕ
inst✝³ : ExpChar F✝ q
inst✝² : IsPurelyInseparable F✝ E✝
inst✝¹ : FiniteDimensional F✝ E✝
F E : Type v
inst✝ : Field F
⊢ ∀ [inst : Field E] [inst_1 : Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E],
    ∃ n, finrank F E = q ^ n
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F✝ : Type u
E✝ : Type v
inst✝⁶ : Field F✝
inst✝⁵ : Field E✝
inst✝⁴ : Algebra F✝ E✝
q : ℕ
inst✝³ : ExpChar F✝ q
inst✝² : IsPurelyInseparable F✝ E✝
inst✝¹ : FiniteDimensional F✝ E✝
F E : Type v
inst✝ : Field F
⊢ ∀ [inst : Field E] [inst_1 : Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E],
    ∃ n, finrank F E = q ^ n

Tactic:
_

Goal state after:
F✝ : Type u
E✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : Field E✝
inst✝⁵ : Algebra F✝ E✝
q : ℕ
inst✝⁴ : ExpChar F✝ q
inst✝³ : IsPurelyInseparable F✝ E✝
inst✝² : FiniteDimensional F✝ E✝
F E : Type v
inst✝¹ : Field F
inst✝ : Field E
⊢ ∀ [inst : Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E],
    ∃ n, finrank F E = q ^ n
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F✝ : Type u
E✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : Field E✝
inst✝⁵ : Algebra F✝ E✝
q : ℕ
inst✝⁴ : ExpChar F✝ q
inst✝³ : IsPurelyInseparable F✝ E✝
inst✝² : FiniteDimensional F✝ E✝
F E : Type v
inst✝¹ : Field F
inst✝ : Field E
⊢ ∀ [inst : Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E],
    ∃ n, finrank F E = q ^ n

Tactic:
_

Goal state after:
F✝ : Type u
E✝ : Type v
inst✝⁸ : Field F✝
inst✝⁷ : Field E✝
inst✝⁶ : Algebra F✝ E✝
q : ℕ
inst✝⁵ : ExpChar F✝ q
inst✝⁴ : IsPurelyInseparable F✝ E✝
inst✝³ : FiniteDimensional F✝ E✝
F E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ n, finrank F E = q ^ n
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F✝ : Type u
E✝ : Type v
inst✝⁸ : Field F✝
inst✝⁷ : Field E✝
inst✝⁶ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁵ : ExpChar F✝ q✝
inst✝⁴ : IsPurelyInseparable F✝ E✝
inst✝³ : FiniteDimensional F✝ E✝
F E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
⊢ ∀ [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ n, finrank F E = q ^ n

Tactic:
_

Goal state after:
F✝ : Type u
E✝ : Type v
inst✝⁹ : Field F✝
inst✝⁸ : Field E✝
inst✝⁷ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁶ : ExpChar F✝ q✝
inst✝⁵ : IsPurelyInseparable F✝ E✝
inst✝⁴ : FiniteDimensional F✝ E✝
F E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
⊢ ∀ [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ n, finrank F E = q ^ n
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F✝ : Type u
E✝ : Type v
inst✝⁹ : Field F✝
inst✝⁸ : Field E✝
inst✝⁷ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁶ : ExpChar F✝ q✝
inst✝⁵ : IsPurelyInseparable F✝ E✝
inst✝⁴ : FiniteDimensional F✝ E✝
F E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
⊢ ∀ [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ n, finrank F E = q ^ n

Tactic:
_

Goal state after:
F✝ : Type u
E✝ : Type v
inst✝¹⁰ : Field F✝
inst✝⁹ : Field E✝
inst✝⁸ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁷ : ExpChar F✝ q✝
inst✝⁶ : IsPurelyInseparable F✝ E✝
inst✝⁵ : FiniteDimensional F✝ E✝
F E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
q : ℕ
inst✝¹ : ExpChar F q
inst✝ : IsPurelyInseparable F E
⊢ ∀ [FiniteDimensional F E], ∃ n, finrank F E = q ^ n
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F✝ : Type u
E✝ : Type v
inst✝¹⁰ : Field F✝
inst✝⁹ : Field E✝
inst✝⁸ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁷ : ExpChar F✝ q✝
inst✝⁶ : IsPurelyInseparable F✝ E✝
inst✝⁵ : FiniteDimensional F✝ E✝
F E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
q : ℕ
inst✝¹ : ExpChar F q
inst✝ : IsPurelyInseparable F E
⊢ ∀ [FiniteDimensional F E], ∃ n, finrank F E = q ^ n

Tactic:
_

Goal state after:
F✝ : Type u
E✝ : Type v
inst✝¹¹ : Field F✝
inst✝¹⁰ : Field E✝
inst✝⁹ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
F E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
q : ℕ
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
⊢ ∃ n, finrank F E = q ^ n
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
halg : Algebra.IsAlgebraic F E
⊢ finSepDegree F E * finInsepDegree F E = finrank F E

Tactic:
have := congr_arg Cardinal.toNat (sepDegree_mul_insepDegree F E)

Goal state after:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
halg : Algebra.IsAlgebraic F E
this : Cardinal.toNat (sepDegree F E * insepDegree F E) = Cardinal.toNat (Module.rank F E)
⊢ finSepDegree F E * finInsepDegree F E = finrank F E
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case inl.tmul
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
a✝ : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x : R
y : K
⊢ ∃ n, x ⊗ₜ[k] y ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range

Tactic:
| tmul x y =>

Goal state after:
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
F : Type u_6
inst✝² : Field F
inst✝¹ : Algebra K F
inst✝ : FiniteDimensional K L
x : L
hF : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
⊢ (algebraMap K F) ((Algebra.trace K L) x) = finrank (↥K⟮x⟯) L • ((minpoly K x).aroots F).sum

Tactic:
trace_eq_trace_adjoin K x,

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
F : Type u_6
inst✝² : Field F
inst✝¹ : Algebra K F
inst✝ : FiniteDimensional K L
x : L
hF : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
⊢ (algebraMap K F) (finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)) =
    finrank (↥K⟮x⟯) L • ((minpoly K x).aroots F).sum
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis hx
⊢ (algebraMap K E) ((Algebra.trace K L) x) = ∑ σ, σ x

Tactic:
trace_eq_trace_adjoin K x,

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis hx
⊢ (algebraMap K E) (finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)) = ∑ σ, σ x
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
⊢ ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff = 0 x

Tactic:
obtain ⟨g, hg₁, m, hg₂⟩ :=
      (minpoly.irreducible (IsIntegral.isIntegral (R := K) x)).hasSeparableContraction p

Goal state after:
case neg
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
m : ℕ
hg₂ : (expand K (p ^ m)) g = minpoly K x
⊢ ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff = 0 x
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h : map (algebraMap A B) p = (X - C b) ^ i * X ^ j
f : B ≃ₐ[A] B
hi : i ≠ 0
⊢ f b = b

Tactic:
by_cases ha : b = 0

Goal state after:
case pos
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h : map (algebraMap A B) p = (X - C b) ^ i * X ^ j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : b = 0
⊢ f b = b

case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h : map (algebraMap A B) p = (X - C b) ^ i * X ^ j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
⊢ f b = b
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ (traceMatrix A ⇑b *ᵥ b.equivFun z) i = (trace A B) (z * b i)

Tactic:
← replicateCol_apply (ι := Fin 1) (traceMatrix A b *ᵥ b.equivFun z) i 0,

Goal state after:
ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ replicateCol (Fin 1) (traceMatrix A ⇑b *ᵥ b.equivFun z) i 0 = (trace A B) (z * b i)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: A : Type u
B : Type v
C : Type z
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : CommRing C
inst✝ : Algebra A C
pb : PowerBasis A B
e : Fin pb.dim ≃ (B →ₐ[A] C)
i j : Fin pb.dim
⊢ embeddingsMatrixReindex A C (⇑pb.basis) e i j = (vandermonde fun i ↦ (e i) pb.gen)ᵀ i j

Tactic:
simp [embeddingsMatrixReindex, embeddingsMatrix]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p : ℕ
left✝ : CharP K p
n : ℕ+
hp : Nat.Prime p
hn : q = p ^ ↑n
⊢ IsPrimePow q

Tactic:
exact ⟨p, n, Nat.prime_iff.mp hp, n.prop, hn.symm⟩

Goal state after:
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  ∑ x, x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    if j = i then 1 else 0
σ : L →ₐ[K] AlgebraicClosure K
⊢ σ ∈ Finset.univ →
    σ ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen)) * pb.gen ^ ↑j) =
      σ pb.gen ^ ↑j / σ ((aeval pb.gen) (derivative (minpoly K pb.gen))) * σ ((minpolyDiv K pb.gen).coeff ↑i)

Tactic:
_

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  ∑ x, x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    if j = i then 1 else 0
σ : L →ₐ[K] AlgebraicClosure K
a✝ : σ ∈ Finset.univ
⊢ σ ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen)) * pb.gen ^ ↑j) =
    σ pb.gen ^ ↑j / σ ((aeval pb.gen) (derivative (minpoly K pb.gen))) * σ ((minpolyDiv K pb.gen).coeff ↑i)
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: case h
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ a = d ^ 2 ∨ a = -d ^ 2

Tactic:
← hu

Goal state after:
case h
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: x n : ℕ
h : x.Coprime n
⊢ x ^ φ n ≡ 1 [MOD n]

Tactic:
rw [← ZMod.natCast_eq_natCast_iff]

Goal state after:
x n : ℕ
h : x.Coprime n
⊢ ↑(x ^ φ n) = ↑1
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : DivisionRing K
inst✝ : CharP K p
⊢ Subfield.map (castHom ⋯ K) ⊤ = Subfield.map ?m.26 ⊥

pp: K : Type u_1
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : DivisionRing K
inst✝ : CharP K p
⊢ ZMod p →+* K

Tactic:
Subsingleton.elim ⊥

Goal state after:
K : Type u_1
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : DivisionRing K
inst✝ : CharP K p
⊢ Subfield.map (castHom ⋯ K) ⊤ = Subfield.map ?m.26 ?m.32

K : Type u_1
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : DivisionRing K
inst✝ : CharP K p
⊢ Subfield (ZMod p)

K : Type u_1
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : DivisionRing K
inst✝ : CharP K p
⊢ ZMod p →+* K
Module: Mathlib.RingTheory.ZMod

Goal state before:
pp: n : ℕ
⊢ IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0

Tactic:
rw [← RingHom.ker_isRadical_iff_reduced_of_surjective
      (ZMod.ringHom_surjective <| Int.castRingHom <| ZMod n),
      ZMod.ker_intCastRingHom, ← isRadical_iff_span_singleton, isRadical_iff_squarefree_or_zero,
      Int.squarefree_natCast, Nat.cast_eq_zero]

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

Goal state before:
pp: n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
⊢ a = 1 ∨ IsUnit (a - 1)

Tactic:
rcases eq_or_ne n 0 with rfl | hn0

Goal state after:
case inl
p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : 0 = p ^ k
a : ZMod 0
ha : (orderOf a).Coprime 0
⊢ a = 1 ∨ IsUnit (a - 1)

case inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
hn0 : n ≠ 0
⊢ a = 1 ∨ IsUnit (a - 1)
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ invFun p (toFun p (Quotient.mk x')) = Quotient.mk x'

Tactic:
dsimp only [toFun, invFun]
    rw [quotientPiLift_mk p, funext fun i => (mkQ_apply (p i) (x' i)), piQuotientLift_mk p,
      lsum_single, id_apply]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
p : α
⊢ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset →
    p ∉ normalizedFactors b → id p ^ Multiset.count p (normalizedFactors b) = 1

Tactic:
_

Goal state after:
case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
p : α
a✝ : p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset
⊢ p ∉ normalizedFactors b → id p ^ Multiset.count p (normalizedFactors b) = 1
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
p : α
⊢ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset →
    p ∉ normalizedFactors a → id p ^ Multiset.count p (normalizedFactors a) = 1

Tactic:
_

Goal state after:
case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
p : α
a✝ : p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset
⊢ p ∉ normalizedFactors a → id p ^ Multiset.count p (normalizedFactors a) = 1