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

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
inst✝¹ : Algebra.IsSeparable F ↥(adjoin F S)
q : ℕ
inst✝ : ExpChar F q
n : ℕ
⊢ adjoin F S = adjoin F ((fun x ↦ x ^ q ^ n) '' S)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
a : E
ha : IsSeparable F a
q : ℕ
inst✝ : ExpChar F q
n : ℕ
⊢ F⟮a⟯ = F⟮a ^ q ^ n⟯

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra.IsSeparable F E
a : E
q : ℕ
inst✝ : ExpChar F q
n : ℕ
⊢ F⟮a⟯ = F⟮a ^ q ^ n⟯

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hM)).range
s : Finset S
hs : Submodule.span R ↑s = M'
⊢ ↑s ⊆ ↑A

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
i : A ⊗[F] B →ₐ[F] K := IsScalarTower.toAlgHom F (A ⊗[F] B) K
fa : A →ₐ[F] K := i.comp Algebra.TensorProduct.includeLeft
fb : B →ₐ[F] K := i.comp Algebra.TensorProduct.includeRight
H : Function.Injective ⇑(fa.range.mulMap fb.range)
⊢ i =
    (fa.range.mulMap fb.range).comp
      ↑(Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa ⋯) (AlgEquiv.ofInjective fb ⋯))

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
⊢ Submodule.span F (Set.range fun x ↦ v x ^ q ^ n) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
i : A ⊗[F] B →ₐ[F] K := IsScalarTower.toAlgHom F (A ⊗[F] B) K
fa : A →ₐ[F] K := i.comp Algebra.TensorProduct.includeLeft
fb : B →ₐ[F] K := i.comp Algebra.TensorProduct.includeRight
H : Function.Injective ⇑(fa.range.mulMap fb.range)
hi :
  i =
    (fa.range.mulMap fb.range).comp
      ↑(Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa ⋯) (AlgEquiv.ofInjective fb ⋯))
⊢ Function.Injective ⇑i

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
h : LinearIndependent F v
h' : LinearIndepOn F id (Set.range v)
ι' : Set E := h'.extend ⋯
b : Basis (↑ι') F E := Basis.extend h'
this : Fintype ↑ι' := FiniteDimensional.fintypeBasisIndex b
H : LinearIndependent F fun (x : ↑ι') ↦ b x ^ q ^ n
f : ι → ↑ι' := fun i ↦ ⟨v i, ⋯⟩
x✝¹ x✝ : ι
heq : f x✝¹ = f x✝
⊢ v x✝¹ = v x✝

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
h : LinearIndependent F v
⊢ LinearIndependent F fun x ↦ v x ^ q ^ n

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
H :
  ∀ (K : Type (max v w)) [inst : Field K] [inst_1 : Algebra F K] (fa : A →ₐ[F] K) (fb : B →ₐ[F] K),
    fa.fieldRange.LinearDisjoint ↥fb.fieldRange
⊢ IsField (A ⊗[F] B)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i✝ : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∉ l.support
⊢ (algebraMap F E) 0 = l i ^ q ^ n

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : LinearIndependent F v
⊢ LinearIndependent F fun x ↦ v x ^ q ^ n

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
E' : IntermediateField F E := adjoin F (Set.range v)
⊢ ∀ x ∈ Set.range v, IsSeparable F x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
K : Type u_1
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsDomain (E ⊗[F] K)
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F K
L : Type (max v u_1)
w✝¹ : Field L
w✝ : Algebra F L
fa : E →ₐ[F] L
fb : K →ₐ[F] L
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
H : fa.range.LinearDisjoint fb.range
⊢ Algebra.IsAlgebraic F ↥fa.fieldRange ∨ Algebra.IsAlgebraic F ↥fb.fieldRange

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i✝ : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
⊢ l i ^ q ^ n ∈ (algebraMap F E).range

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
⊢ LinearIndependent F fun x ↦ v x ^ q ^ n

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q : ℕ
hF : ExpChar F q
inst✝ : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
⊢ minpoly F ((iterateFrobenius E q n) a) = Polynomial.map (iterateFrobenius F q n) (minpoly F a)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q : ℕ
hF : ExpChar F q
inst✝ : ExpChar E q
a : E
hsep : IsSeparable F a
⊢ minpoly F ((frobenius E q) a) = Polynomial.map (frobenius F q) (minpoly F a)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h✝ : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
x : F
y : E
h : (frobenius E p) y = (algebraMap F E) x
⊢ (algebraMap F E) x = y ^ ringExpChar F ^ 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i✝ : ι
f : ι → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
lF : ι → F
hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n
i : ι
⊢ lF i ≠ 0 → i ∈ l.support

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
A B : IntermediateField F E
inst✝ : FiniteDimensional F E
h₁ : A.LinearDisjoint ↥B
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ (Algebra.trace (↥A) E) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.trace F ↥B) x)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h✝ : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this✝ : ExpChar E p
x z : F
h : (frobenius E p) ((algebraMap F E) z) = (algebraMap F E) x
this : (Algebra.ofId F E).toRingHom z ∈ perfectClosure F E
⊢ (algebraMap F E) ((frobenius F p) z) = (algebraMap F E) x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
x : F
⊢ ∃ a, (frobenius F p) a = x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : PerfectField E
eq : perfectClosure F E = ⊥
⊢ PerfectField F

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
⊢ intDegree 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
⊢ intDegree 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
k : K
⊢ (C k).intDegree = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
⊢ X.intDegree = 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
p : K[X]
⊢ ((algebraMap K[X] K⟮X⟯) p).intDegree = ↑p.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).intDegree = x.intDegree + y.intDegree

Tactic:
simp only [intDegree, add_sub, sub_add, sub_sub_eq_add_sub, sub_sub, sub_eq_sub_iff_add_eq_add]

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(x * y).num.natDegree + (↑x.denom.natDegree + ↑y.denom.natDegree) =
    ↑x.num.natDegree + ↑y.num.natDegree + ↑(x * y).denom.natDegree
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
i : ι
f : ι → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
lF : ι → F
hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
hl : ∑ i ∈ l.support, (l i • v i) ^ q ^ n = 0
x✝ : ι
⊢ 0 • v x✝ ^ q ^ n = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).intDegree = x.intDegree + y.intDegree

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
A B : IntermediateField F E
inst✝ : FiniteDimensional F E
h₁ : A.LinearDisjoint ↥B
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ (Algebra.norm ↥A) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.norm F) x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hM)).range
s : Finset S
hs : Submodule.span R ↑s = M'
hs' : ↑s ⊆ ↑A
A' : Subalgebra R S := Algebra.adjoin R ↑s
hf' : Module.Finite R ↥A'
hA : toSubmodule A' ≤ toSubmodule A
x✝ : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hx : x✝ ∈ {x, y}
⊢ x✝ ∈ ↑(LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)).range

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
⊢ x⁻¹.intDegree = -x.intDegree

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ (x / y).intDegree = x.intDegree - y.intDegree

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
g : K⟮X⟯
x✝ : g ∈ ⊤
⊢ g = (aeval X) g.num / (aeval X) g.denom

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ {X} ⊆ ↑E ∪ {X}

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ (↥E)⟮ X⟯ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝⁹ : Field K
f : K⟮X⟯
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra K A
inst✝⁶ : Algebra (↥K[f]) A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra K B
inst✝³ : Algebra (↥K[f]) B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower K A B
inst✝ : IsScalarTower (↥K[f]) A B
⊢ Polynomial.map (algebraMap A B) (f.minpolyX A) = f.minpolyX B

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : K
⊢ (C x).minpolyX ↥K⟮C x⟯ = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
⊢ (-x).intDegree = x.intDegree

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
s : K[X]
hs : s ≠ 0
⊢ ↑(x.num * s).natDegree - ↑(s * x.denom).natDegree = x.intDegree

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
⊢ (aeval X) (f.minpolyX ↥K⟮f⟯) = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ↑((f.minpolyX ↥K⟮f⟯).coeff f.denom.natDegree) = 0
⊢ ∃ c, f = C c

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
h : f.minpolyX ↥K⟮f⟯ = 0
⊢ ↑((f.minpolyX ↥K⟮f⟯).coeff f.denom.natDegree) = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
⊢ (∃ c, f = C c) → f.minpolyX ↥K⟮f⟯ = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i : ι
f : ι → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
lF : ι → F
hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
⊢ (Finsupp.linearCombination F fun x ↦ v x ^ q ^ n) lF₀ = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
⊢ Algebra.IsAlgebraic (↥K⟮f⟯) K⟮X⟯

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
⊢ (x + y).intDegree ≤ max x.intDegree y.intDegree

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
⊢ f ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
⊢ LinearIndependent E v

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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✝¹ : IsPurelyInseparable F E
S : IntermediateField F K
inst✝ : Algebra.IsSeparable F ↥S
ι : Set ↥S
b : Module.Basis (↑ι) F ↥S
i : ↑ι
⊢ IsSeparable F ((⇑S.val ∘ ⇑b) i)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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✝¹ : IsPurelyInseparable F E
inst✝ : Algebra.IsSeparable E K
⊢ sepDegree F K = Module.rank E K

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
⊢ f.num.natDegree ≤ (f.minpolyX ↥K⟮f⟯).natDegree

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

Goal state before:
pp: F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
⊢ Module.rank F E * sepDegree E K = sepDegree F K

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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
⊢ insepDegree F K = insepDegree E K

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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✝ : IsPurelyInseparable F E
⊢ sepDegree F K = sepDegree E K

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
M' : Submodule R S
hM : M' ≤ toSubmodule A
hf : Module.Finite R ↥M'
s : Finset S
hs : Submodule.span R ↑s = M'
hs' : ↑s ⊆ ↑A
A' : Subalgebra R S := Algebra.adjoin R ↑s
hf' : Module.Finite R ↥A'
hA : toSubmodule A' ≤ toSubmodule A
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)).range
x' : ↥(toSubmodule A') ⊗[R] ↥(toSubmodule B)
hx' : (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) x' = x
y' : ↥(toSubmodule A') ⊗[R] ↥(toSubmodule B)
hy' : (LinearMap.rTensor (↥(toSubmodule B)) (Submodule.inclusion hA)) y' = y
⊢ ((toSubmodule A').mulMap (toSubmodule B)) x' = ((toSubmodule A').mulMap (toSubmodule B)) y'

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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✝ : IsPurelyInseparable F E
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
⊢ A.LinearDisjoint B

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

Goal state before:
pp: F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
⊢ Module.rank F E * insepDegree E K = insepDegree F K

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Field R
inst✝¹ : Ring S
inst✝ : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
hc : ∀ (a b : ↥A), Commute ↑a ↑b
⊢ A = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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.IsAlgebraic F E
⊢ Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)

Tactic:
by

Goal state after: