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

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).leadingCoeff * (X - C x).leadingCoeff ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ ¬minpolyDiv R x = 0
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 q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' : Polynomial.map (algebraMap R K) d' * C r.leadingCoeff = r
⊢ (Polynomial.map (algebraMap R K) q * r).Monic

Tactic:
simpa using

Goal state after:
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 q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' : Polynomial.map (algebraMap R K) d' * C r.leadingCoeff = r
⊢ (Polynomial.map (algebraMap R K) p).Monic
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_2
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)).Monic

Tactic:
simpa using

Goal state after:
case refine_2
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (minpoly K ((algebraMap S L) s)).Monic
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_4
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (minpoly K ((algebraMap S L) s)).scaleRoots 1 ∣
    (minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)).scaleRoots ((algebraMap R K) r)⁻¹

Tactic:
scaleRoots_one

Goal state after:
case refine_4
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ minpoly K ((algebraMap S L) s) ∣
    (minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)).scaleRoots ((algebraMap R K) r)⁻¹
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_4
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (Polynomial.aeval ((algebraMap S L) s))
      ((minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)).scaleRoots ((algebraMap R K) r)⁻¹) =
    0

Tactic:
← inv_mul_cancel_left₀ (b := algebraMap S L s)
      (a := algebraMap K L (algebraMap R K r)) (by simpa),

Goal state after:
case refine_4
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (Polynomial.aeval
        (((algebraMap K L) ((algebraMap R K) r))⁻¹ * ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)))
      ((minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)).scaleRoots ((algebraMap R K) r)⁻¹) =
    0
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: 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
x : S
hx : IsIntegral R x
P : R[X]
hP₁ : (Minpoly.toAdjoin R x) ((AdjoinRoot.mk (minpoly R x)) P) = 0
⊢ (AdjoinRoot.mk (minpoly R x)) P = 0

Tactic:
simpa using

Goal state after:
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
x : S
hx : IsIntegral R x
P : R[X]
hP₁ : (Minpoly.toAdjoin R x) ((AdjoinRoot.mk (minpoly R x)) P) = 0
⊢ minpoly R x ∣ P
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
hdeg : f.degree ≠ 0
hsep : f.Separable
x : k
hx : f.IsRoot x
⊢ a * x ^ n + b * x + c = 0

Tactic:
simpa using

Goal state after:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
hdeg : f.degree ≠ 0
hsep : f.Separable
x : k
hx : f.IsRoot x
⊢ a * x ^ n + b * x + c = 0
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: case h
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : (X ^ n - C x).degree ≠ 0
hx : ¬x = 0
z : k
hz : (X ^ n - C x).IsRoot z
⊢ z ^ n = x

Tactic:
simpa using

Goal state after:
case h
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : (X ^ n - C x).degree ≠ 0
hx : ¬x = 0
z : k
hz : (X ^ n - C x).IsRoot z
⊢ z ^ n = x
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hp : Irreducible p
hs : p.Separable
x : k
hx : eval x (p * C p.leadingCoeff⁻¹) = 0
⊢ eval x p = 0

Tactic:
simpa using

Goal state after:
k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hp : Irreducible p
hs : p.Separable
x : k
hx : eval x (p * C p.leadingCoeff⁻¹) = 0
⊢ eval x p = 0
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsSepClosed E
h : separableClosure F E = ⊥
p : F[X]
x✝ : p.Monic
hirr : Irreducible p
hsep : p.Separable
x : F
hx : (aeval ((Algebra.ofId F E).toRingHom x)) p = 0
⊢ eval x p = 0

Tactic:
simpa using

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsSepClosed E
h : separableClosure F E = ⊥
p : F[X]
x✝ : p.Monic
hirr : Irreducible p
hsep : p.Separable
x : F
hx : (aeval ((Algebra.ofId F E).toRingHom x)) p = 0
⊢ eval x p = 0
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
K : Type u_3
inst✝² : Ring K
inst✝¹ : Algebra F K
e : K ≃ₐ[F] E
inst✝ : IsPurelyInseparable F K
x : E
h : (minpoly F (e.symm x)).Separable
⊢ x ∈ (algebraMap F E).range

Tactic:
simpa using

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
K : Type u_3
inst✝² : Ring K
inst✝¹ : Algebra F K
e : K ≃ₐ[F] E
inst✝ : IsPurelyInseparable F K
x : E
h : (minpoly F (e.symm x)).Separable
⊢ ∃ x_1, (algebraMap F E) x_1 = x
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
⊢ IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
isPurelyInseparable_iff

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
⊢ (∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)) ↔
    ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
x : E
g : F[X]
h1 : g.Separable
n : ℕ
h2 : (expand F (q ^ n)) g = minpoly F x
⊢ (aeval (x ^ q ^ n)) g = 0

Tactic:
simpa using

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Ring E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
h : ∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
x : E
g : F[X]
h1 : g.Separable
n : ℕ
h2 : (expand F (q ^ n)) g = minpoly F x
⊢ (aeval (x ^ q ^ n)) g = 0
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ (trace R R) 1 = LinearMap.id 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ (trace R R) 1 = 1
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(adjoin k {x}).toIntermediateField/k) :=
  fun x ↦ Subgroup.map (restrictNormalHom ↥(adjoin k {x}).toIntermediateField) L.fixingSubgroup
f : ↥L → IntermediateField k K := fun x ↦ IntermediateField.lift (IntermediateField.fixedField (g ↑x))
this✝ : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal k ↥(f l)
n : Normal k ↥(⨆ l, f l)
l : ↥L
⊢ f l ≤ L

Tactic:
simpa using

Goal state after:
case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(adjoin k {x}).toIntermediateField/k) :=
  fun x ↦ Subgroup.map (restrictNormalHom ↥(adjoin k {x}).toIntermediateField) L.fixingSubgroup
f : ↥L → IntermediateField k K := fun x ↦ IntermediateField.lift (IntermediateField.fixedField (g ↑x))
this✝ : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal k ↥(f l)
n : Normal k ↥(⨆ l, f l)
l : ↥L
⊢ L ⊓ (adjoin k {↑l}).toIntermediateField ≤ L
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
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
q : ℕ
h2✝ : ∀ (x : K), ∃ n, x ^ q ^ n ∈ (algebraMap E K).range
h1✝ : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
h✝ : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : (algebraMap E K) y = x ^ q ^ n
m : ℕ
z : F
h1 : (algebraMap F E) z = y ^ q ^ m
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap F K).range

Tactic:
refine ⟨n + m, z, ?_⟩

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
q : ℕ
h2✝ : ∀ (x : K), ∃ n, x ^ q ^ n ∈ (algebraMap E K).range
h1✝ : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
h✝ : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : (algebraMap E K) y = x ^ q ^ n
m : ℕ
z : F
h1 : (algebraMap F E) z = y ^ q ^ m
⊢ (algebraMap F K) z = x ^ q ^ (n + m)
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(adjoin k {x}).toIntermediateField/k) := ⋯
f : ↥L → IntermediateField k K := ⋯
this✝ : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal k ↥(f l)
n : Normal k ↥(⨆ l, f l)
l : K
hl : l ∈ L
⊢ l ∈ f ⟨l, hl⟩

Tactic:
simpa using

Goal state after:
case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(adjoin k {x}).toIntermediateField/k) :=
  fun x ↦ Subgroup.map (restrictNormalHom ↥(adjoin k {x}).toIntermediateField) L.fixingSubgroup
f : ↥L → IntermediateField k K := fun x ↦ IntermediateField.lift (IntermediateField.fixedField (g ↑x))
this✝ : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal k ↥(f l)
n : Normal k ↥(⨆ l, f l)
l : K
hl : l ∈ L
⊢ l ∈ (adjoin k {l}).toIntermediateField
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsGalois k ↥L
⊢ L.fixingSubgroup.Normal

Tactic:
simpa using

Goal state after:
case refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsGalois k ↥L
⊢ (restrictNormalHom ↥L).ker.Normal
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
this :
  ∀ (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
⊢ ∃ n, finrank F E = q ^ n

Tactic:
simpa using

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
this :
  ∀ (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
⊢ ∃ 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
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
⊢ IsPurelyInseparable F E

Tactic:
isPurelyInseparable_iff

Goal state after:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
⊢ ∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case h
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
r : R[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * (mapRingHom (algebraMap R K)) r
⊢ q = p * r

Tactic:
simpa using

Goal state after:
case h
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
r : R[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * (mapRingHom (algebraMap R K)) r
⊢ q = p * r
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
L : Type u_3
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this : DecidableEq L := Classical.decEq L
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis (↥(IsNoetherian.finsetBasisIndex K L)) K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ x ∈ Finset.image (⇑bs') Finset.univ, IsIntegral A (y • x)
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap A K))

Tactic:
exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)

Goal state after:
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
hG : IsGaloisGroup G A B
H : Type u_5
inst✝¹ : Group H
inst✝ : MulSemiringAction H B
e : H ≃* G
he : ∀ (h : H) (x : B), e h • x = h • x
x : H
a : A
b : B
⊢ x • a • b = a • x • b

Tactic:
simpa using

Goal state after:
G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
hG : IsGaloisGroup G A B
H : Type u_5
inst✝¹ : Group H
inst✝ : MulSemiringAction H B
e : H ≃* G
he : ∀ (h : H) (x : B), e h • x = h • x
x : H
a : A
b : B
⊢ x • a • b = a • x • b
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
hG : IsGaloisGroup G A B
H : Type u_5
inst✝¹ : Group H
inst✝ : MulSemiringAction H B
e : H ≃* G
he : ∀ (h : H) (x : B), e h • x = h • x
b : B
h : ∀ (g : H), g • b = b
he' : ∀ (g : G) (x : B), e.symm g • x = g • x
g : G
⊢ g • b = b

Tactic:
simpa using

Goal state after:
G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
hG : IsGaloisGroup G A B
H : Type u_5
inst✝¹ : Group H
inst✝ : MulSemiringAction H B
e : H ≃* G
he : ∀ (h : H) (x : B), e h • x = h • x
b : B
h : ∀ (g : H), g • b = b
he' : ∀ (g : G) (x : B), e.symm g • x = g • x
g : G
⊢ g • b = b
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁷ : Group G
inst✝⁶ : CommSemiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
inst✝³ : MulSemiringAction G B
hG : IsGaloisGroup G A B
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
m₁✝ m₂✝ : G
h : ∀ (a : B'), m₁✝ • a = m₂✝ • a
b : B
⊢ m₁✝ • b = m₂✝ • b

Tactic:
simpa using

Goal state after:
G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁷ : Group G
inst✝⁶ : CommSemiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
inst✝³ : MulSemiringAction G B
hG : IsGaloisGroup G A B
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
m₁✝ m₂✝ : G
h : ∀ (a : B'), m₁✝ • a = m₂✝ • a
b : B
⊢ m₁✝ • b = m₂✝ • b
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁷ : Group G
inst✝⁶ : CommSemiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
inst✝³ : MulSemiringAction G B
hG : IsGaloisGroup G A B
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
g : G
a : A
b' : B'
h' : ∀ {x' : B'}, e.symm (g • x') = g • e.symm x'
⊢ e.symm (g • a • b') = e.symm (a • g • b')

Tactic:
simpa using

Goal state after:
G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁷ : Group G
inst✝⁶ : CommSemiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
inst✝³ : MulSemiringAction G B
hG : IsGaloisGroup G A B
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
g : G
a : A
b' : B'
h' : ∀ {x' : B'}, e.symm (g • x') = g • e.symm x'
⊢ g • a • e.symm b' = a • g • e.symm b'
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁵ : Group G
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : MulSemiringAction G B
hA : IsGaloisGroup G A B
inst✝ : FaithfulSMul A B
x : ↥(FixedPoints.subsemiring B G)
⊢ (fun x ↦ ⟨(algebraMap A B) x, ⋯⟩) ((fun x ↦ ⋯.choose) x) = x

Tactic:
simpa using

Goal state after:
G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁵ : Group G
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : MulSemiringAction G B
hA : IsGaloisGroup G A B
inst✝ : FaithfulSMul A B
x : ↥(FixedPoints.subsemiring B G)
⊢ (algebraMap A B) ⋯.choose = ↑x
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
x : L
hx : ¬IsIntegral K x
⊢ (Algebra.trace K ↥K⟮x⟯) (gen K x) = 0

Tactic:
trace_eq_zero_of_not_exists_basis,

Goal state after:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ¬IsIntegral K x
⊢ 0 (gen K x) = 0

case h
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ¬IsIntegral K x
⊢ ¬∃ s, Nonempty (Basis (↥s) K ↥K⟮x⟯)
Module: Mathlib.Data.Nat.Prime.Int

Goal state before:
pp: p : ℕ
hp : _root_.Prime ↑p
a b : ℕ
⊢ p ∣ a * b → p ∣ a ∨ p ∣ b

Tactic:
simpa using

Goal state after:
p : ℕ
hp : _root_.Prime ↑p
a b : ℕ
⊢ p ∣ a * b → p ∣ a ∨ p ∣ b
Module: Mathlib.Data.Nat.Prime.Int

Goal state before:
pp: p q : ℕ
hp : Prime p
hq : Prime q
m : ℕ
hm : m + 1 ≠ 0
n : ℕ
hn : n + 1 ≠ 0
h : p ^ (m + 1) = q ^ (n + 1)
⊢ p = q ∧ m + 1 = n + 1

Tactic:
simpa using

Goal state after:
p q : ℕ
hp : Prime p
hq : Prime q
m : ℕ
hm : m + 1 ≠ 0
n : ℕ
hn : n + 1 ≠ 0
h : p ^ (m + 1) = q ^ (n + 1)
⊢ p = q ∧ m = n
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
x : L
hx : IsIntegral K x
⊢ (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x) = -(minpoly K x).nextCoeff

Tactic:
simpa using

Goal state after:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x) = -(minpoly K x).nextCoeff
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ e ((trace A C) x) = 0 x

Tactic:
trace_eq_zero_of_not_exists_basis,

Goal state after:
case neg
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ e (0 x) = 0 x

case neg.h
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
⊢ ¬∃ s, Nonempty (Basis (↥s) A C)
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a b : ZMod n
h : a.valMinAbs = -b.valMinAbs
⊢ a = -b

Tactic:
rcases eq_zero_or_neZero n with rfl | hn <;> simp_all [valMinAbs_spec]

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

Goal state before:
pp: A₁ : Type u_7
B₁ : Type u_8
A₂ : Type u_9
B₂ : Type u_10
inst✝⁵ : CommRing A₁
inst✝⁴ : CommRing B₁
inst✝³ : CommRing A₂
inst✝² : CommRing B₂
inst✝¹ : Algebra A₁ B₁
inst✝ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
x : B₁
⊢ (trace A₁ B₁) x = e₁.symm ((trace A₂ B₂) (e₂ x))

Tactic:
let := (RingHom.comp (e₂ : B₁ →+* B₂) (algebraMap A₁ B₁)).toAlgebra
  let e' : B₁ ≃ₐ[A₁] B₂ := { e₂ with commutes' := fun _ ↦ rfl }
  rw [← Algebra.trace_eq_of_ringEquiv e₁ he, ← Algebra.trace_eq_of_algEquiv e',
    RingEquiv.symm_apply_apply]
  rfl

Goal state after: