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

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
inst✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this✝⁴ : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ IntermediateField.restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : (minpoly (↥E') x).Separable
this✝³ : Algebra.IsSeparable F ↥E'
this✝² : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯
this✝¹ : FiniteDimensional ↥E' ↥(↥E')⟮x⟯
this✝ : FiniteDimensional F ↥(↥E')⟮x⟯
this : finSepDegree F ↥E' * finSepDegree ↥E' ↥(↥E')⟮x⟯ = finSepDegree F ↥(↥E')⟮x⟯
⊢ IsSeparable F x

Tactic:
rw [finSepDegree_eq_finrank_of_isSeparable F E',
    finSepDegree_eq_finrank_of_isSeparable E' E'⟮x⟯,
    Module.finrank_mul_finrank F E' E'⟮x⟯,
    eq_comm, finSepDegree_eq_finrank_iff F E'⟮x⟯] at this

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
inst✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this✝⁴ : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ IntermediateField.restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : (minpoly (↥E') x).Separable
this✝³ : Algebra.IsSeparable F ↥E'
this✝² : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯
this✝¹ : FiniteDimensional ↥E' ↥(↥E')⟮x⟯
this✝ : FiniteDimensional F ↥(↥E')⟮x⟯
this : Algebra.IsSeparable F ↥(↥E')⟮x⟯
⊢ IsSeparable F x
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E
inst✝³ : Algebra F E'
inst✝² : Algebra E E'
inst✝¹ : IsScalarTower F E E'
L : IntermediateField F E
inst✝ : Normal F E
f : Gal(E'/F)
⊢ (∀ x ∈ map (IsScalarTower.toAlgHom F E E') L, f x = x) ↔ ∀ x ∈ L, ((restrictNormalHom E) f) x = x

Tactic:
constructor

Goal state after:
case mp
F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E
inst✝³ : Algebra F E'
inst✝² : Algebra E E'
inst✝¹ : IsScalarTower F E E'
L : IntermediateField F E
inst✝ : Normal F E
f : Gal(E'/F)
⊢ (∀ x ∈ map (IsScalarTower.toAlgHom F E E') L, f x = x) → ∀ x ∈ L, ((restrictNormalHom E) f) x = x

case mpr
F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E
inst✝³ : Algebra F E'
inst✝² : Algebra E E'
inst✝¹ : IsScalarTower F E E'
L : IntermediateField F E
inst✝ : Normal F E
f : Gal(E'/F)
⊢ (∀ x ∈ L, ((restrictNormalHom E) f) x = x) → ∀ x ∈ map (IsScalarTower.toAlgHom F E E') L, f x = x
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
inst✝ : IsGalois F E'
L : IntermediateField F E'
hnfd : FiniteDimensional F ↥L
E : IntermediateField F E' := normalClosure F (↥L) E'
hle : L ≤ E
L' : IntermediateField F ↥E := restrict hle
h : finrank F ↥L' * Nat.card ↥L'.fixingSubgroup = L'.fixingSubgroup.index * Nat.card ↥L'.fixingSubgroup
⊢ finrank F ↥L = L.fixingSubgroup.index

Tactic:
Nat.mul_left_inj Finite.card_pos.ne'

Goal state after:
F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
inst✝ : IsGalois F E'
L : IntermediateField F E'
hnfd : FiniteDimensional F ↥L
E : IntermediateField F E' := normalClosure F (↥L) E'
hle : L ≤ E
L' : IntermediateField F ↥E := restrict hle
h : finrank F ↥L' = L'.fixingSubgroup.index
⊢ finrank F ↥L = L.fixingSubgroup.index
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
hB : B.Nondegenerate
inst✝ : IsTorsionFree R S
N : Submodule R M
hN : Submodule.span S ↑N = ⊤
x y : ↥(B.dualSubmodule N)
e : (B.dualSubmoduleToDual N) x = (B.dualSubmoduleToDual N) y
⊢ x = y

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
hB : B.Nondegenerate
inst✝ : IsTorsionFree R S
N : Submodule R M
hN : Submodule.span S ↑N = ⊤
x y : ↥(B.dualSubmodule N)
e : (B.dualSubmoduleToDual N) x = (B.dualSubmoduleToDual N) y
⊢ ↑x = ↑y
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this : ∀ (n : ℕ), (map (algebraMap K g.SplittingField) g).coeff n ∈ ↑(integralClosure R g.SplittingField).toSubring
n : ℕ
p : R[X]
hp : p.Monic
he : eval₂ (algebraMap R g.SplittingField) ((map (algebraMap K g.SplittingField) g).coeff n) p = 0
⊢ eval₂ (algebraMap R K) (g.coeff n) p = 0

Tactic:
rw [IsScalarTower.algebraMap_eq R K, coeff_map, ← eval₂_map, eval₂_at_apply] at he

Goal state after:
case right
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this : ∀ (n : ℕ), (map (algebraMap K g.SplittingField) g).coeff n ∈ ↑(integralClosure R g.SplittingField).toSubring
n : ℕ
p : R[X]
hp : p.Monic
he : (algebraMap K g.SplittingField) (eval (g.coeff n) (map (algebraMap R K) p)) = 0
⊢ eval₂ (algebraMap R K) (g.coeff n) p = 0
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case h
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
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a ↦ σ • a = a
⊢ σ • ↑(adjoin k {y}).fixingSubgroup ⊆ (↑L.fixingSubgroup)ᶜ ∧
    IsOpen (σ • ↑(adjoin k {y}).fixingSubgroup) ∧ σ ∈ σ • ↑(adjoin k {y}).fixingSubgroup

Tactic:
constructor

Goal state after:
case h.left
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
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a ↦ σ • a = a
⊢ σ • ↑(adjoin k {y}).fixingSubgroup ⊆ (↑L.fixingSubgroup)ᶜ

case h.right
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
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a ↦ σ • a = a
⊢ IsOpen (σ • ↑(adjoin k {y}).fixingSubgroup) ∧ σ ∈ σ • ↑(adjoin k {y}).fixingSubgroup
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
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit ((mapRingHom (algebraMap R K)) b' * C b.leadingCoeff)

Tactic:
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]))

Goal state after:
case refine_1
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
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ p = a' * b'

case refine_2
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
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ ¬IsUnit a'
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
xL : x ∈ L
h : ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩
σ : Gal(K/k)
hσ : σ ∈ H
⊢ ↑(((restrictNormalHom ↥L) σ) ⟨x, xL⟩) = x

Tactic:
h σ hσ

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
xL : x ∈ L
h : ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩
σ : Gal(K/k)
hσ : σ ∈ H
⊢ ↑⟨x, xL⟩ = x
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✝ : IsDomain R
⊢ IsIntegrallyClosed R ↔ ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))

Tactic:
constructor

Goal state after:
case mp
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
⊢ IsIntegrallyClosed R → ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))

case mpr
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
⊢ (∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))) → IsIntegrallyClosed R
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_3
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
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
x✝ : C p.leadingCoeff ∣ p
q : R[X]
hMul : p = C p.leadingCoeff * q
⊢ ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → q.degree ≤ Q.degree

Tactic:
exact (hMul ▸ degree_C_mul <| by simp [h₀]) ▸ pmin

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_3
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 S L) s))
      ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)) =
    0

Tactic:
exact scaleRoots_aeval_eq_zero (minpoly.aeval _ _)

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

Tactic:
exact scaleRoots_aeval_eq_zero (minpoly.aeval _ _)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : ¬∃ s, Nonempty (Basis (↥s) R S)
s : S
⊢ (trace R S) s = 0 s

Tactic:
simp [trace_apply, LinearMap.trace, h]

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

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

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ (trace R R) 1 = LinearMap.id 1
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), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
x : E
hdeg : (minpoly F x).natSepDegree = 1
h' : ¬IsIntegral F x
⊢ False

Tactic:
simp only [minpoly.eq_zero h', natSepDegree_zero, zero_ne_one] at hdeg

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

Goal state before:
pp: case intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
x : T
this✝ : DecidableEq ι
this : DecidableEq κ
val✝¹ : Fintype ι
val✝ : Fintype κ
⊢ ((leftMulMatrix b) ((trace S T) x)).trace = ((leftMulMatrix (b.smulTower c)) x).trace

Tactic:
trace_eq_matrix_trace c,

Goal state after:
case intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
x : T
this✝ : DecidableEq ι
this : DecidableEq κ
val✝¹ : Fintype ι
val✝ : Fintype κ
⊢ ((leftMulMatrix b) ((leftMulMatrix c) x).trace).trace = ((leftMulMatrix (b.smulTower c)) x).trace
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
⊢ trace R S ∘ₗ ↑R (trace S T) = trace R T

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
x✝ : T
⊢ (trace R S ∘ₗ ↑R (trace S T)) x✝ = (trace R T) x✝
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case refine_1
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
this : ⨆ l, f l = L
⊢ IsGalois k ↥L

Tactic:
constructor

Goal state after:
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
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f ↦ f.comp (algebraMap F E)
this : Algebra E L := (Classical.arbitrary (E →+* L)).toAlgebra
j : AlgebraicClosure E →ₐ[E] L := IsAlgClosed.lift
f g : Emb F E
⊢ (fun f ↦ f.comp (algebraMap F E)) (j.comp ↑f) = (fun f ↦ f.comp (algebraMap F E)) (j.comp ↑g)

Tactic:
ext

Goal state after:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f ↦ f.comp (algebraMap F E)
this : Algebra E L := (Classical.arbitrary (E →+* L)).toAlgebra
j : AlgebraicClosure E →ₐ[E] L := IsAlgClosed.lift
f g : Emb F E
x✝ : F
⊢ ((fun f ↦ f.comp (algebraMap F E)) (j.comp ↑f)) x✝ = ((fun f ↦ f.comp (algebraMap F E)) (j.comp ↑g)) x✝
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
C : Type u_4
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
⊢ IsNoetherian A C

Tactic:
by
  have := Classical.decEq L
  obtain ⟨s, b, hb_int⟩ := FiniteDimensional.exists_is_basis_integral A K L
  let b' := (traceForm K L).dualBasis (traceForm_nondegenerate K L) b
  let := isNoetherian_span_of_finite A (Set.finite_range b')
  let f : C →ₗ[A] Submodule.span A (Set.range b') :=
    (Submodule.inclusion (IsIntegralClosure.range_le_span_dualBasis C b hb_int)).comp
      ((Algebra.linearMap C L).restrictScalars A).rangeRestrict
  refine isNoetherian_of_ker_bot f ?_
  rw [LinearMap.ker_comp, Submodule.ker_inclusion, Submodule.comap_bot, LinearMap.ker_codRestrict]
  exact LinearMap.ker_eq_bot_of_injective (IsIntegralClosure.algebraMap_injective C A L)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : PowerBasis R S
⊢ (LinearMap.BilinForm.toMatrix h.basis) (traceForm R S) = of fun i j ↦ (trace R S) (h.gen ^ (↑i + ↑j))

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : PowerBasis R S
i✝ j✝ : Fin h.dim
⊢ (LinearMap.BilinForm.toMatrix h.basis) (traceForm R S) i✝ j✝ = of (fun i j ↦ (trace R S) (h.gen ^ (↑i + ↑j))) i✝ j✝
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
⊢ ⟨f ↑1, ⋯⟩ = 1

Tactic:
ext

Goal state after:
K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
⊢ ↑⟨f ↑1, ⋯⟩ = ↑1
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
x y : 𝓞 K
⊢ ⟨f ↑(x * y), ⋯⟩ = ⟨f ↑x, ⋯⟩ * ⟨f ↑y, ⋯⟩

Tactic:
ext

Goal state after:
K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
x y : 𝓞 K
⊢ ↑⟨f ↑(x * y), ⋯⟩ = ↑(⟨f ↑x, ⋯⟩ * ⟨f ↑y, ⋯⟩)
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
⊢ ⟨f ↑0, ⋯⟩ = 0

Tactic:
ext

Goal state after:
K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
⊢ ↑⟨f ↑0, ⋯⟩ = ↑0
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
x y : 𝓞 K
⊢ ⟨f ↑(x + y), ⋯⟩ = ⟨f ↑x, ⋯⟩ + ⟨f ↑y, ⋯⟩

Tactic:
ext

Goal state after:
K✝ : Type u_1
L✝ : Type u_2
inst✝³ : Field K✝
inst✝² : Field L✝
K : Type u_3
L : Type u_4
inst✝¹ : Field K
inst✝ : Field L
f : K →+* L
x y : 𝓞 K
⊢ ↑⟨f ↑(x + y), ⋯⟩ = ↑(⟨f ↑x, ⋯⟩ + ⟨f ↑y, ⋯⟩)
Module: Mathlib.RingTheory.IsGaloisGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝⁹ : Group G
H : Subgroup G
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Semiring C
inst✝⁶ : Algebra A C
inst✝⁵ : MulSemiringAction G C
N : Subgroup G
inst✝⁴ : CommSemiring B
inst✝³ : Algebra B C
inst✝² : FaithfulSMul B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
this : SMul G B := smulOfNormal G B C N
⊢ MulSemiringAction G B

Tactic:
have : SMulDistribClass G B C := smulDistribClass_smulOfNormal G B C N

Goal state after:
G : Type u_1
inst✝⁹ : Group G
H : Subgroup G
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Semiring C
inst✝⁶ : Algebra A C
inst✝⁵ : MulSemiringAction G C
N : Subgroup G
inst✝⁴ : CommSemiring B
inst✝³ : Algebra B C
inst✝² : FaithfulSMul B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
this✝ : SMul G B := smulOfNormal G B C N
this : SMulDistribClass G B C
⊢ MulSemiringAction G B
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos
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
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ ((minpoly K ((algebraMap (↥K⟮x⟯) L) (gen K x))).aroots F).sum = ((minpoly K x).aroots F).sum

Tactic:
try simp only [AdjoinSimple.algebraMap_gen _ _]

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

Goal state before:
pp: case pos
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
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K ((algebraMap (↥K⟮x⟯) L) (gen K x)))).Splits

Tactic:
try simp only [AdjoinSimple.algebraMap_gen _ _]

Goal state after:
case pos
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
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case e_6
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A B
inst✝ : Algebra A C
e : B ≃ₐ[A] C
x : B
⊢ (lmul A C) (e x) = (↑e).conj ((lmul A B) x)

Tactic:
ext

Goal state after:
case e_6
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A B
inst✝ : Algebra A C
e : B ≃ₐ[A] C
x : B
x✝ : C
⊢ ((lmul A C) (e x)) x✝ = ((↑e).conj ((lmul A B) x)) x✝
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ -(↑n * 2) < x.valMinAbs * 2 - y * 2 ∧ x.valMinAbs * 2 - y * 2 < ↑n * 2

Tactic:
constructor

Goal state after:
case h2.left
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ -(↑n * 2) < x.valMinAbs * 2 - y * 2

case h2.right
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ x.valMinAbs * 2 - y * 2 < ↑n * 2
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ a.valMinAbs.natAbs = b.valMinAbs.natAbs ↔ a = b ∨ a = -b

Tactic:
constructor

Goal state after:
case mp
n : ℕ
a b : ZMod n
⊢ a.valMinAbs.natAbs = b.valMinAbs.natAbs → a = b ∨ a = -b

case mpr
n : ℕ
a b : ZMod n
⊢ a = b ∨ a = -b → a.valMinAbs.natAbs = b.valMinAbs.natAbs