mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type ?u.5
S : Type ?u.7
M : Type ?u.9
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
N : Submodule R M
y : M
x✝ : y ∈ N
⊢ 0 ∈ 1

Tactic:
;

Goal state after:
R : Type ?u.5
S : Type ?u.7
M : Type ?u.9
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
N : Submodule R M
y : M
x✝ : y ∈ N
⊢ 0 ∈ 1
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case refine_2
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
⊢ g.coeff n ∈ ↑(integralClosure R K).toSubring

Tactic:
;

Goal state after:
case refine_2
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
⊢ g.coeff n ∈ ↑(integralClosure R K).toSubring
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 : (algebraMap K g.SplittingField) (eval (g.coeff n) (map (algebraMap R K) p)) = 0
⊢ eval (g.coeff n) (map (algebraMap R K) p) = 0

Tactic:
;

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 (g.coeff n) (map (algebraMap R K) p) = 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
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
x : ↥(integralClosure R K)
⊢ ((algebraMap R K).comp (↑algeq).toRingHom) x = (integralClosure R K).toSubring.subtype x

Tactic:
;

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
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
x : ↥(integralClosure R K)
⊢ ((algebraMap R K).comp (↑algeq).toRingHom) x = (integralClosure R K).toSubring.subtype 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✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
x : ↥(integralClosure R K)
⊢ ((algebraMap R K).comp (↑algeq).toRingHom) x = (integralClosure R K).toSubring.subtype (algeq.symm (algeq x))

Tactic:
;

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
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
x : ↥(integralClosure R K)
⊢ ((algebraMap R K).comp (↑algeq).toRingHom) x = (integralClosure R K).toSubring.subtype (algeq.symm (algeq x))
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
i : ℕ
⊢ (minpolyDiv R x).coeff i = (minpolyDiv R x * (X - C x)).coeff (i + 1) + (minpolyDiv R x).coeff (i + 1) * x

Tactic:
;

Goal state after:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
⊢ (minpolyDiv R x).coeff i = (minpolyDiv R x * (X - C x)).coeff (i + 1) + (minpolyDiv R x).coeff (i + 1) * x
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
⊢ eval x (minpolyDiv R x) = eval x (derivative (minpolyDiv R x * (X - C x)))

Tactic:
;

Goal state after:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ eval x (minpolyDiv R x) = eval x (derivative (minpolyDiv R x * (X - C x)))
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
i : ℕ
H : (minpolyDiv R x).coeff i ∉ R[x]
j : ℕ
⊢ (minpolyDiv R x).coeff (i + j) ∉ R[x]

Tactic:
;

Goal state after:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ R[x]
j : ℕ
⊢ (minpolyDiv R x).coeff (i + j) ∉ R[x]
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H✝ : (minpolyDiv R x).coeff i ∉ R[x]
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ R[x]
H : (minpolyDiv R x).coeff (i + (j + 1)) ∈ R[x]
⊢ False

Tactic:
;

Goal state after:
case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H✝ : (minpolyDiv R x).coeff i ∉ R[x]
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ R[x]
H : (minpolyDiv R x).coeff (i + (j + 1)) ∈ R[x]
⊢ False
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
s : S
P : R[X]
hmo : P.Monic
hP : (Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree
hs : IsIntegral R s
⊢ minpoly R s = P

Tactic:
;

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
s : S
P : R[X]
hmo : P.Monic
hP : (Polynomial.aeval s) P = 0
Pmin : ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree
hs : IsIntegral R s
⊢ minpoly R s = P
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
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
this : ↑(((restrictNormalHom ↥L) σ) ⟨x, xL⟩) = x
⊢ σ x = ↑(((restrictNormalHom ↥L) σ) ⟨x, xL⟩)

Tactic:
exact (AlgEquiv.restrictNormal_commutes σ L ⟨x, xL⟩).symm

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: 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
hR : IsIntegrallyClosed R
p : R[X]
hp : p.Monic
⊢ Irreducible p ↔ Irreducible (map (algebraMap R K) p)

Tactic:
;

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
hR : IsIntegrallyClosed R
p : R[X]
hp : p.Monic
⊢ Irreducible p ↔ Irreducible (map (algebraMap R K) p)
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 : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
⊢ (restrictNormalHom ↥L'.toIntermediateField) σ ∈
    (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)).fixingSubgroup

Tactic:
apply (mem_fixingSubgroup_iff (L' ≃ₐ[k] L')).mpr

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K := ⋯
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
⊢ ∀ y ∈ ↑(fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)),
    (restrictNormalHom ↥L'.toIntermediateField) σ • y = y
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case pos
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpolyDiv R x).natDegree + 1 - 1

Tactic:
;

Goal state after:
case pos
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpolyDiv R x).natDegree + 1 - 1
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case neg
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : ¬IsIntegral R x
⊢ natDegree 0 = natDegree 0 - 1

Tactic:
;

Goal state after:
case neg
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : ¬IsIntegral R x
⊢ natDegree 0 = natDegree 0 - 1
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
⊢ ∃ x, eval x p = 0

Tactic:
exact ⟨x, by simpa [hp.ne_zero] using hx⟩

Goal state after:
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
⊢ IsIntegral F (e.symm x✝)

Tactic:
;

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
⊢ IsIntegral F (e.symm x✝)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly

Goal state before:
pp: case inl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Subsingleton R
⊢ ((leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen

pp: case inr
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ ((leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen

Tactic:
;

Goal state after:
case inl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Subsingleton R
⊢ ((leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen

case inr
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
⊢ ((leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly

Goal state before:
pp: case inr.hl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
q : R[X]
h0 : ¬q = 0
hq : (aeval h.gen) q = 0
⊢ ↑h.dim ≤ q.degree

Tactic:
;

Goal state after:
case inr.hl
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : Ring S
inst✝ : Algebra R S
h : PowerBasis R S
h✝ : Nontrivial R
q : R[X]
h0 : ¬q = 0
hq : (aeval h.gen) q = 0
⊢ ↑h.dim ≤ q.degree
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:
;

Goal state after:
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
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
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ ((toMatrix b b) ((lmul R S) s)).trace = ((toMatrix b b) (mulLeft R s)).trace

Tactic:
;

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

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

Tactic:
;

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✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
⊢ Algebra.IsSeparable F ↥(separableClosure F E) ∧ IsPurelyInseparable (↥(separableClosure F E)) E

Tactic:
;

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
⊢ Algebra.IsSeparable F ↥(separableClosure F E) ∧ IsPurelyInseparable (↥(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
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✝

Tactic:
;

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.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
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x : R
⊢ (algebraMap R A) x ∈ (algebraMap R A).rangeS

Tactic:
;

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
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x : R
⊢ (algebraMap R A) x ∈ (algebraMap R A).rangeS
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: case refine_1
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)
hy' : (algebraMap A L) y ≠ 0
x : L
⊢ (fun x ↦ ((algebraMap A L) y)⁻¹ * x) ((fun x ↦ (algebraMap A L) y * x) x) = x

Tactic:
;

Goal state after:
case refine_1
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)
hy' : (algebraMap A L) y ≠ 0
x : L
⊢ (fun x ↦ ((algebraMap A L) y)⁻¹ * x) ((fun x ↦ (algebraMap A L) y * x) x) = x
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: case refine_2
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)
hy' : (algebraMap A L) y ≠ 0
x : L
⊢ (fun x ↦ (algebraMap A L) y * x) ((fun x ↦ ((algebraMap A L) y)⁻¹ * x) x) = x

Tactic:
;

Goal state after:
case refine_2
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)
hy' : (algebraMap A L) y ≠ 0
x : L
⊢ (fun x ↦ (algebraMap A L) y * x) ((fun x ↦ ((algebraMap A L) y)⁻¹ * x) x) = 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:
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.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: 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
x : R ⊗[k] K
q : ℕ := ringExpChar k
⊢ ∃ n > 0, x ^ n ∈ (algebraMap R (R ⊗[k] K)).range

Tactic:
obtain ⟨n, hr⟩ := exists_pow_pow_mem_range_tensorProduct_of_expChar q x

Goal state after:
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
x : R ⊗[k] K
q : ℕ := ringExpChar k
n : ℕ
hr : x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range
⊢ ∃ n > 0, x ^ n ∈ (algebraMap R (R ⊗[k] K)).range
Module: Mathlib.RingTheory.IsGaloisGroup.Basic

Goal state before:
pp: G : Type u_1
B : Type u_3
inst✝⁴ : Group G
inst✝³ : Semiring B
inst✝² : MulSemiringAction G B
C : Type u_4
inst✝¹ : CommSemiring C
inst✝ : Algebra C B
N : Subgroup G
hN : N.Normal
hC : IsGaloisGroup (↥N) C B
g : G
x : C
n : ↥N
⊢ g⁻¹ • ↑n • g • (algebraMap C B) x = (algebraMap C B) x

Tactic:
← mul_smul,

Goal state after:
G : Type u_1
B : Type u_3
inst✝⁴ : Group G
inst✝³ : Semiring B
inst✝² : MulSemiringAction G B
C : Type u_4
inst✝¹ : CommSemiring C
inst✝ : Algebra C B
N : Subgroup G
hN : N.Normal
hC : IsGaloisGroup (↥N) C B
g : G
x : C
n : ↥N
⊢ (g⁻¹ * ↑n) • g • (algebraMap C B) x = (algebraMap C B) x
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
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✝

Tactic:
;

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:
;

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:
;

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, ⋯⟩)