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

Goal state before:
pp: p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝² : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst✝¹ : Field E
inst✝ : Algebra K E
x : E
hx : minpoly K x = X ^ p - C a
h : ¬IsIntegral K x
⊢ False

Tactic:
simpa using

Goal state after:
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝² : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst✝¹ : Field E
inst✝ : Algebra K E
x : E
hx : minpoly K x = X ^ p - C a
h : ¬IsIntegral K x
⊢ False
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
hp' : p ≠ 2
n : ℕ
a : K
ha : ∀ (b : K), b ^ p ≠ a
q : ℕ
hq : Nat.Prime q
hq' : q ∣ p ^ n
⊢ ∀ (b : K), b ^ q ≠ a

Tactic:
simpa using

Goal state after:
K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
hp' : p ≠ 2
n : ℕ
a : K
ha : ∀ (b : K), b ^ p ≠ a
q : ℕ
hq : Nat.Prime q
hq' : q ∣ p ^ n
⊢ ∀ (b : K), ¬b ^ p = a
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁶ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a✝ : K
H : Irreducible (X ^ n - C a✝)
L✝ : Type u_1
inst✝⁵ : Field L✝
inst✝⁴ : Algebra K L✝
inst✝³ : IsSplittingField K L✝ (X ^ n - C a✝)
α : L✝
hα : α ^ n = (algebraMap K L✝) a✝
hn : 0 < n
a : K
L : Type ?u.56
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
⊢ (Polynomial.map (algebraMap K L) (X ^ n - C a)).degree ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u
inst✝⁶ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a✝ : K
H : Irreducible (X ^ n - C a✝)
L✝ : Type u_1
inst✝⁵ : Field L✝
inst✝⁴ : Algebra K L✝
inst✝³ : IsSplittingField K L✝ (X ^ n - C a✝)
α : L✝
hα : α ^ n = (algebraMap K L✝) a✝
hn : 0 < n
a : K
L : Type ?u.56
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
⊢ ¬n = 0
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
this : eval (rootOfSplits ⋯ ⋯) (Polynomial.map (algebraMap K L) (X ^ n - C a)) = 0
⊢ rootOfSplitsXPowSubC ⋯ a L ^ n = (algebraMap K L) a

Tactic:
simpa using

Goal state after:
K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
this : eval (rootOfSplits ⋯ ⋯) (Polynomial.map (algebraMap K L) (X ^ n - C a)) = 0
⊢ rootOfSplitsXPowSubC ⋯ a L ^ n = (algebraMap K L) a
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
inst✝ : NeZero n
σ : Gal(L/K)
ζ : K
hα : α ∈ Multiset.map (fun x ↦ (algebraMap K L) ζ ^ x * rootOfSplitsXPowSubC ⋯ a L) (Multiset.range n)
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α

Tactic:
simp only [Multiset.mem_map, Multiset.mem_range] at hα

Goal state after:
K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
inst✝ : NeZero n
σ : Gal(L/K)
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
hα : ∃ a_1 < n, (algebraMap K L) ζ ^ a_1 * rootOfSplitsXPowSubC ⋯ a L = α
⊢ (autEquivRootsOfUnity ⋯ H L) σ • α = σ α
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(L/K)
ζ : K
hζ'✝ : ζ ∈ primitiveRoots n K
hζ' : IsPrimitiveRoot ζ n
hn : 0 < n
i : ℕ
left✝ : i < n
⊢ (autEquivRootsOfUnity ⋯ H L) σ • ζ ^ i • rootOfSplitsXPowSubC ⋯ a L =
    ζ ^ i • (autEquivRootsOfUnity hζ H L) σ • rootOfSplitsXPowSubC ⋯ a L

Tactic:
exact smul_comm _ _ _

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
m : ℕ
⊢ ((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α

Tactic:
simpa using

Goal state after:
K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
m : ℕ
⊢ ((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ' : orderOf σ = finrank K L
⊢ (minpoly K σ.toLinearMap).IsRoot ζ

Tactic:
simpa using

Goal state after:
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ' : orderOf σ = finrank K L
⊢ ζ ^ finrank K L = 1
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : ι → ↥A
i : (ι →₀ ↥B) →ₗ[R] S := Submodule.mulLeftMap (toSubmodule B) a
j : (ι →₀ ↥B) →ₗ[R] S :=
  ↑(MulOpposite.opLinearEquiv R).symm ∘ₗ
    ↑R (Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)) ∘ₗ
      ↑(Finsupp.mapRange.linearEquiv B.linearEquivOp)
this : i = j
⊢ Function.Injective ⇑(↑R (Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a))) ↔
    Function.Injective ⇑(Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a))

Tactic:
LinearMap.coe_restrictScalars

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : ι → ↥A
i : (ι →₀ ↥B) →ₗ[R] S := Submodule.mulLeftMap (toSubmodule B) a
j : (ι →₀ ↥B) →ₗ[R] S :=
  ↑(MulOpposite.opLinearEquiv R).symm ∘ₗ
    ↑R (Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)) ∘ₗ
      ↑(Finsupp.mapRange.linearEquiv B.linearEquivOp)
a✝ : ι
x✝ : ↥B
⊢ (i ∘ₗ Finsupp.lsingle a✝) x✝ = (j ∘ₗ Finsupp.lsingle a✝) x✝

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply, coe_val,
    Finsupp.mapRange.linearEquiv_toLinearMap, LinearEquiv.coe_coe,
    MulOpposite.coe_opLinearEquiv_symm, LinearMap.coe_restrictScalars,
    Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single, Finsupp.linearCombination_single,
    MulOpposite.unop_smul, MulOpposite.unop_op, i, j]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : ι → ↥A
i : (ι →₀ ↥B) →ₗ[R] S := Submodule.mulLeftMap (toSubmodule B) a
j : (ι →₀ ↥B) →ₗ[R] S :=
  ↑(MulOpposite.opLinearEquiv R).symm ∘ₗ
    ↑R (Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)) ∘ₗ
      ↑(Finsupp.mapRange.linearEquiv B.linearEquivOp)
a✝ : ι
x✝ : ↥B
⊢ (Submodule.mulLeftMap (toSubmodule B) a) (Finsupp.single a✝ x✝) = B.linearEquivOp x✝ • ↑(a a✝)
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
⊢ ∑ i ∈ s, (↑(H i).index)⁻¹ < 1

Tactic:
| inr hs =>

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : L
⊢ mk K x✝ = 0 ↔ x✝ ∈ {0}

Tactic:
mk_eq_zero_iff,

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : L
⊢ x✝ = 0 ↔ x✝ ∈ {0}
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : ConjRootClass K L
⊢ (∃ a, mk K a = x ∧ ∃ b, mk K b = y ∧ a + b = 0) → x = -y

Tactic:
rintro ⟨a, rfl, b, rfl, h⟩

Goal state after:
case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a b : L
h : a + b = 0
⊢ mk K a = -mk K b
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
c : ConjRootClass K L
⊢ Irreducible c.minpoly

Tactic:
induction c
  rw [minpoly_mk]
  exact minpoly.irreducible (Algebra.IsIntegral.isIntegral _)

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

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x x✝ : L
⊢ (aeval x) (mk K x✝).minpoly = 0 ↔ mk K x = mk K x✝

Tactic:
simpa using

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x x✝ : L
⊢ IsConjRoot K x✝ x ↔ IsConjRoot K x x✝
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁷ : CommRing R
A : Type v
inst✝⁶ : CommRing A
B : Type w
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Flat R A
inst✝¹ : Flat R B
inst✝ : IsDomain (A ⊗[R] B)
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
K : Type (max w v) := FractionRing (A ⊗[R] B)
i : A ⊗[R] B →ₐ[R] K := IsScalarTower.toAlgHom R (A ⊗[R] B) K
hi : Function.Injective ⇑i
⊢ (i.comp Algebra.TensorProduct.includeLeft).range.LinearDisjoint (i.comp Algebra.TensorProduct.includeRight).range

Tactic:
simpa using

Goal state after:
R : Type u
inst✝⁷ : CommRing R
A : Type v
inst✝⁶ : CommRing A
B : Type w
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Flat R A
inst✝¹ : Flat R B
inst✝ : IsDomain (A ⊗[R] B)
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
K : Type (max w v) := FractionRing (A ⊗[R] B)
i : A ⊗[R] B →ₐ[R] K := IsScalarTower.toAlgHom R (A ⊗[R] B) K
hi : Function.Injective ⇑i
⊢ (Subalgebra.map i Algebra.TensorProduct.includeLeft.range).LinearDisjoint
    (Subalgebra.map i Algebra.TensorProduct.includeRight.range)
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 : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L'
inst✝⁴ : Algebra L' L
inst✝³ : IsScalarTower F L' L
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L' E
inst✝ : IsScalarTower L' L E
⊢ A.LinearDisjoint L'

Tactic:
refine Subalgebra.LinearDisjoint.of_le_right_of_flat H ?_

Goal state after:
F : Type u
E : Type v
inst✝¹³ : Field F
inst✝¹² : Field E
inst✝¹¹ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L'
inst✝⁴ : Algebra L' L
inst✝³ : IsScalarTower F L' L
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L' E
inst✝ : IsScalarTower L' L E
⊢ (IsScalarTower.toAlgHom F L' E).range ≤ (IsScalarTower.toAlgHom F L E).range
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
x : S
y : T
⊢ (includeLeft.toLinearMap.range.mulMap includeRight.toLinearMap.range ∘ₗ
        _root_.TensorProduct.map includeLeft.toLinearMap.rangeRestrict includeRight.toLinearMap.rangeRestrict)
      (x ⊗ₜ[R] y) =
    LinearMap.id (x ⊗ₜ[R] y)

Tactic:
rw [LinearMap.comp_apply, LinearMap.id_apply, _root_.TensorProduct.map_tmul]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
x : S
y : T
⊢ (includeLeft.toLinearMap.range.mulMap includeRight.toLinearMap.range)
      (includeLeft.toLinearMap.rangeRestrict x ⊗ₜ[R] includeRight.toLinearMap.rangeRestrict y) =
    x ⊗ₜ[R] y
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: case refine_2
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
i : E →ₐ[F] K
x : E
x✝ : ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range
n : ℕ
y : F
h : (algebraMap F E) y = x ^ ringExpChar F ^ n
⊢ (algebraMap F K) y = i x ^ ringExpChar F ^ n

Tactic:
simpa using

Goal state after:
case refine_2
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
i : E →ₐ[F] K
x : E
x✝ : ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range
n : ℕ
y : F
h : (algebraMap F E) y = x ^ ringExpChar F ^ n
⊢ (algebraMap F K) y = i x ^ ringExpChar F ^ n
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 : IntermediateField F E
L : Type v
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Module.rank ↥A ↥(extendScalars ⋯) = Module.rank F L

Tactic:
simpa using

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type v
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Module.rank ↥A ↥(extendScalars ⋯) = Module.rank F L
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 : IntermediateField F E
L : Type v
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Module.rank F L * Module.rank (↥(adjoin L ↑A)) E = Module.rank (↥A) E

Tactic:
simpa using

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type v
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Module.rank F L * Module.rank (↥(adjoin L ↑A)) E = Module.rank (↥A) E
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 : ℕ
this : Algebra.IsSeparable F ↥F⟮a⟯
⊢ F⟮a⟯ = F⟮a ^ q ^ n⟯

Tactic:
simpa using

Goal state after:
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 : ℕ
this : Algebra.IsSeparable F ↥F⟮a⟯
⊢ F⟮a⟯ = F⟮a ^ q ^ n⟯
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:
simpa using

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

Goal state after:
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✝
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 rw [map_zero, Finsupp.notMem_support_iff.1 hs, zero_pow this]

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:
simpa using

Goal state after:
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)
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.toSubalgebra
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ A.toSubalgebra ⊔ B.toSubalgebra = ⊤

Tactic:
simpa using

Goal state after:
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.toSubalgebra
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ A.toSubalgebra ⊔ B.toSubalgebra = ⊤
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

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

Tactic:
simpa using

Goal state after:
case h
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ↑((f.minpolyX ↥K⟮f⟯).coeff f.denom.natDegree) = 0
⊢ C (f.num.coeff f.denom.natDegree) = f * C f.denom.leadingCoeff
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:
simpa using

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

Goal state after:
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
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
this :
  (f.minpolyX ↥K⟮f⟯).natDegree ≤
    max f.num.natDegree
      (Polynomial.C ((algebraMap ↥K[f] ↥K⟮f⟯) ⟨f, ⋯⟩) * Polynomial.map (algebraMap K ↥K⟮f⟯) f.denom).natDegree
H : (algebraMap ↥K[f] ↥K⟮f⟯) ⟨f, ⋯⟩ = 0
⊢ f = C 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
this :
  (f.minpolyX ↥K⟮f⟯).natDegree ≤
    max f.num.natDegree
      (Polynomial.C ((algebraMap ↥K[f] ↥K⟮f⟯) ⟨f, ⋯⟩) * Polynomial.map (algebraMap K ↥K⟮f⟯) f.denom).natDegree
H : (algebraMap ↥K[f] ↥K⟮f⟯) ⟨f, ⋯⟩ = 0
⊢ f = 0
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.IsAlgebraic F E
⊢ sepDegree F E * sepDegree E K = sepDegree F K

Tactic:
simpa using

Goal state after:
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.IsAlgebraic F E
⊢ sepDegree F E * sepDegree E K = sepDegree F K
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.IsAlgebraic F E
⊢ insepDegree F E * insepDegree E K = insepDegree F K

Tactic:
simpa using

Goal state after:
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.IsAlgebraic F E
⊢ insepDegree F E * insepDegree E K = insepDegree F K
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.IsAlgebraic F E
⊢ insepDegree F E * insepDegree E K = insepDegree F K

Tactic:
simpa only [Cardinal.lift_id] using lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic F E K

Goal state after: