awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
h : ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
x : E
hdeg : natSepDegree (minpoly F x) = 1
halg : IsIntegral F x
hsep : IsSeparable F x
refine_2 :
  ∀ (hdeg : natDegree (minpoly F x) = 1) (halg : IsIntegral F x) (hsep : IsSeparable F x),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
refine_2₁ refine_2₂ refine_2₃ refine_2₄ :
  ∀ (hdeg : Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x) (halg : IsIntegral F x)
    (hsep : IsSeparable F x), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x

Tactic:
rwa [hsep.natSepDegree_eq_natDegree, minpoly.natDegree_eq_one_iff] at hdeg

Premises used: Polynomial.Separable.natSepDegree_eq_natDegree, minpoly.natDegree_eq_one_iff
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Ring E
inst_2 : IsDomain E
inst_3 : Algebra F E
q : ℕ
inst_4 : ExpChar F q
x : E
inst_5 : IsPurelyInseparable F E
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)

Tactic:
(isPurelyInseparable_iff_pow_mem F q).1 ‹_› x

Premises used: isPurelyInseparable_iff_pow_mem, Iff.mp
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F K
⊢ IsPurelyInseparable F E

Tactic:
⟨⟨fun x ↦ (isIntegral' F (algebraMap E K x)).tower_bot_of_field⟩, fun x h ↦ ?_⟩

Premises used: Algebra.algebraMap, IsPurelyInseparable.isIntegral', IsPurelyInseparable.mk, Algebra.IsIntegral.mk, DFunLike.coe, IsIntegral.tower_bot_of_field
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F K
refine :
  ∀ (x : E) (h : IsSeparable F x), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
⊢ IsPurelyInseparable F E

Tactic:
refine ⟨⟨fun x ↦ (isIntegral' F (algebraMap E K x)).tower_bot_of_field⟩, fun x h ↦ ?_⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F K
x : E
h : IsSeparable F x
⊢ Separable (minpoly.{u, w} F (B := K) ((algebraMap E K : (a : E) → K) x : K))

Tactic:
rw [IsSeparable, ← minpoly.algebraMap_eq (algebraMap E K).injective] at h

Premises used: Algebra.algebraMap, RingHom.injective, IsSeparable, minpoly.algebraMap_eq
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F K
x : E
h : Separable (minpoly.{u, w} F (B := K) ((algebraMap E K : (a : E) → K) x : K))
obtain :
  ∀ (y : F)
    (h : Eq.{w + 1} (α := K) (((algebraMap F K : F →+* K) : (a : F) → K) y : K) ((algebraMap E K : (a : E) → K) x : K)),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x

Tactic:
obtain ⟨y, h⟩ := inseparable F _ h

Premises used: IsPurelyInseparable.inseparable
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F K
x : E
h_1 : Separable (minpoly.{u, w} F (B := K) ((algebraMap E K : (a : E) → K) x : K))
y : F
h : Eq.{w + 1} (α := K) (((algebraMap F K : F →+* K) : (a : F) → K) y : K) ((algebraMap E K : (a : E) → K) x : K)
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x

Tactic:
⟨y, (algebraMap E K).injective (h.symm ▸ (IsScalarTower.algebraMap_apply F E K y).symm)⟩

Premises used: Algebra.algebraMap, Set.Mem, setOf, Eq.rec, RingHom.injective, Exists.intro, Set.range, Eq.symm, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F K
x : E
h_1 : Separable (minpoly.{u, w} F (B := K) ((algebraMap E K : (a : E) → K) x : K))
y : F
h : Eq.{w + 1} (α := K) (((algebraMap F K : F →+* K) : (a : F) → K) y : K) ((algebraMap E K : (a : E) → K) x : K)
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) x

Tactic:
exact ⟨y, (algebraMap E K).injective (h.symm ▸ (IsScalarTower.algebraMap_apply F E K y).symm)⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h : IsPurelyInseparable F K
obtain : ∀ (q : ℕ), ExpChar F q → IsPurelyInseparable E K
⊢ IsPurelyInseparable E K

Tactic:
obtain ⟨q, _⟩ := ExpChar.exists F

Premises used: ExpChar.exists
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h : IsPurelyInseparable F K
q : ℕ
h_1 : ExpChar F q
⊢ ExpChar E q

Tactic:
haveI := expChar_of_injective_algebraMap (algebraMap F E).injective q
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h : IsPurelyInseparable F K
q : ℕ
h_1 : ExpChar F q
this : ExpChar E q
rw :
  ∀
    (h :
      ∀ (x : K),
        ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)),
    ExpChar F q →
      ∀ (this : ExpChar E q) (x : K),
        ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
⊢ IsPurelyInseparable E K

Tactic:
rw [isPurelyInseparable_iff_pow_mem _ q] at h ⊢

Premises used: isPurelyInseparable_iff_pow_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h : ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)
h_1 : ExpChar F q
this : ExpChar E q
x : K
obtain :
  ∀ (n : ℕ) (y : F) (h : ((algebraMap F K : F →+* K) : (a : F) → K) y = x ^ q ^ n),
    ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)

Tactic:
obtain ⟨n, y, h⟩ := h x
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h_1 : ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)
h_2 : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : F
h : ((algebraMap F K : F →+* K) : (a : F) → K) y = x ^ q ^ n
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)

Tactic:
⟨n, (algebraMap F E) y, h.symm ▸ (IsScalarTower.algebraMap_apply F E K y).symm⟩

Premises used: Algebra.algebraMap, Eq.rec, Exists.intro, Eq.symm, DFunLike.coe, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h_1 : ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)
h_2 : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : F
h : ((algebraMap F K : F →+* K) : (a : F) → K) y = x ^ q ^ n
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)

Tactic:
exact ⟨n, (algebraMap F E) y, h.symm ▸ (IsScalarTower.algebraMap_apply F E K y).symm⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h1 : IsPurelyInseparable F E
h2 : IsPurelyInseparable E K
obtain : ∀ (q : ℕ), ExpChar F q → IsPurelyInseparable F K
⊢ IsPurelyInseparable F K

Tactic:
obtain ⟨q, _⟩ := ExpChar.exists F

Premises used: ExpChar.exists
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h1 : IsPurelyInseparable F E
h2 : IsPurelyInseparable E K
q : ℕ
h : ExpChar F q
⊢ ExpChar E q

Tactic:
haveI := expChar_of_injective_algebraMap (algebraMap F E).injective q
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h1 : IsPurelyInseparable F E
h2 : IsPurelyInseparable E K
q : ℕ
h : ExpChar F q
this : ExpChar E q
rw :
  ∀
    (h2 :
      ∀ (x : K),
        ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n))
    (h1 :
      ∀ (x : E),
        ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)),
    ExpChar F q →
      ∀ (this : ExpChar E q) (x : K),
        ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)
⊢ IsPurelyInseparable F K

Tactic:
rw [isPurelyInseparable_iff_pow_mem _ q] at h1 h2 ⊢

Premises used: isPurelyInseparable_iff_pow_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h2 : ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
h1 : ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
h : ExpChar F q
this : ExpChar E q
x : K
obtain :
  ∀ (n : ℕ) (y : E) (h2 : ((algebraMap E K : E →+* K) : (a : E) → K) y = x ^ q ^ n),
    ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)

Tactic:
obtain ⟨n, y, h2⟩ := h2 x
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h2_1 :
  ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
h1 : ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
h : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : ((algebraMap E K : E →+* K) : (a : E) → K) y = x ^ q ^ n
obtain :
  ∀ (m : ℕ) (z : F) (h1 : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ m),
    ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)

Tactic:
obtain ⟨m, z, h1⟩ := h1 y
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h2_1 :
  ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
h1_1 :
  ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
h : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : ((algebraMap E K : E →+* K) : (a : E) → K) y = x ^ q ^ n
m : ℕ
z : F
h1 : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ m
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)

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

Premises used: HAdd.hAdd, Exists.intro
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h2_1 :
  ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
h1_1 :
  ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
h : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : ((algebraMap E K : E →+* K) : (a : E) → K) y = x ^ q ^ n
m : ℕ
z : F
h1 : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ m
refine : ((algebraMap F K : F →+* K) : (a : F) → K) z = x ^ q ^ (n + m)
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{u, w} (R := F) (algebraMap F K)) (x ^ q ^ n)

Tactic:
refine ⟨n + m, z, ?_⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
q : ℕ
h2_1 :
  ∀ (x : K), ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range.{v, w} (R := E) (algebraMap E K)) (x ^ q ^ n)
h1_1 :
  ∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)
h : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : ((algebraMap E K : E →+* K) : (a : E) → K) y = x ^ q ^ n
m : ℕ
z : F
h1 : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ m
rw : (algebraMap E K : (a : E) → K) ((algebraMap F E : (a : F) → E) z : E) = x ^ q ^ (n + m)
rw₁ : (algebraMap E K : (a : E) → K) (y ^ q ^ m) = x ^ q ^ (n + m)
rw₂ : HPow.hPow (α := K) ((algebraMap E K : (a : E) → K) y : K) (q ^ m) = x ^ q ^ (n + m)
rw₃ : (x ^ q ^ n) ^ q ^ m = x ^ q ^ (n + m)
rw₄ : x ^ (q ^ n * q ^ m) = x ^ q ^ (n + m)
rw₅ rw₆ : x ^ q ^ (n + m) = x ^ q ^ (n + m)
⊢ ((algebraMap F K : F →+* K) : (a : F) → K) z = x ^ q ^ (n + m)

Tactic:
rw [IsScalarTower.algebraMap_apply F E K, h1, map_pow, h2, ← pow_mul, ← pow_add]

Premises used: pow_add, map_pow, pow_mul, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
M : IntermediateField F K
inst_5 : IsPurelyInseparable F K
⊢ IsPurelyInseparable.{u, w} F ↥M

Tactic:
IsPurelyInseparable.tower_bot F M K

Premises used: Membership.mem, Subtype, IsPurelyInseparable.tower_bot
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
M : IntermediateField F K
inst_5 : IsPurelyInseparable F K
⊢ IsPurelyInseparable (↥M) K

Tactic:
IsPurelyInseparable.tower_top F M K

Premises used: Membership.mem, Subtype, IsPurelyInseparable.tower_top
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
obtain : ∀ (q : ℕ), ExpChar F q → (IsPurelyInseparable F E ↔ ∀ (x : E), natSepDegree (minpoly F x) = 1)
⊢ IsPurelyInseparable F E ↔ ∀ (x : E), natSepDegree (minpoly F x) = 1

Tactic:
obtain ⟨q, _⟩ := ExpChar.exists F

Premises used: ExpChar.exists
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
h : ExpChar F q
simp_rw :
  (∀ (x : E), ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E)) (x ^ q ^ n)) ↔
    ∀ (x : E), natSepDegree (minpoly F x) = 1
⊢ IsPurelyInseparable F E ↔ ∀ (x : E), natSepDegree (minpoly F x) = 1

Tactic:
simp_rw [isPurelyInseparable_iff_pow_mem F q, minpoly.natSepDegree_eq_one_iff_pow_mem q]

Premises used: isPurelyInseparable_iff_pow_mem, minpoly.natSepDegree_eq_one_iff_pow_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsPurelyInseparable F E
x : E
⊢ natSepDegree (minpoly F x) = 1

Tactic:
(isPurelyInseparable_iff_natSepDegree_eq_one F).1 ‹_› x

Premises used: isPurelyInseparable_iff_natSepDegree_eq_one, Iff.mp
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
hF : ExpChar F q
simp_rw :
  (∀ (x : E), natSepDegree (minpoly F x) = 1) ↔
    ∀ (x : E),
      ∃ (n : ℕ) (y : F),
        minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])
⊢ IsPurelyInseparable F E ↔
    ∀ (x : E),
      ∃ (n : ℕ) (y : F),
        minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])

Tactic:
simp_rw [isPurelyInseparable_iff_natSepDegree_eq_one,
    minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C q]

Premises used: minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C, isPurelyInseparable_iff_natSepDegree_eq_one
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
inst_3 : ExpChar F q
inst_4 : IsPurelyInseparable F E
x : E
⊢ ∃ (n : ℕ) (y : F),
    minpoly F x = HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X (q ^ n)) ((C : (a : F) → F[X]) y : F[X])

Tactic:
(isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C F q).1 ‹_› x

Premises used: isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C, Iff.mp
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
hF : ExpChar F q
simp_rw :
  (∀ (x : E), natSepDegree (minpoly F x) = 1) ↔
    ∀ (x : E),
      ∃ (n : ℕ),
        Polynomial.map (algebraMap F E) (minpoly F x) =
          HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n
⊢ IsPurelyInseparable F E ↔
    ∀ (x : E),
      ∃ (n : ℕ),
        Polynomial.map (algebraMap F E) (minpoly F x) =
          HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n

Tactic:
simp_rw [isPurelyInseparable_iff_natSepDegree_eq_one,
    minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow q]

Premises used: minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow, isPurelyInseparable_iff_natSepDegree_eq_one
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
inst_3 : ExpChar F q
inst_4 : IsPurelyInseparable F E
x : E
⊢ ∃ (n : ℕ),
    Polynomial.map (algebraMap F E) (minpoly F x) =
      HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) x : E[X]) ^ q ^ n

Tactic:
(isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow F q).1 ‹_› x

Premises used: isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow, Iff.mp
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
inst_3 : ExpChar F q
inst_4 : IsPurelyInseparable F E
inst_5 : FiniteDimensional F E
this :
  ∀ (F E : Type v) [inst : Field F] [inst_6 : Field E] [inst_7 : Algebra F E] (q : ℕ) [ExpChar F q]
    [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ (n : ℕ), finrank F E = q ^ n
⊢ ∃ (n : ℕ), finrank F E = q ^ n

Tactic:
simpa using this (⊥ : IntermediateField F E) E q

Premises used: Membership.mem, Subtype, Bot.bot
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
inst_3 : ExpChar F q
inst_4 : IsPurelyInseparable F E
inst_5 : FiniteDimensional F E
suffices :
  ∀ (F E : Type v) [inst : Field F] [inst_6 : Field E] [inst_7 : Algebra F E] (q : ℕ) [ExpChar F q]
    [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ (n : ℕ), finrank F E = q ^ n
⊢ ∃ (n : ℕ), finrank F E = q ^ n

Tactic:
suffices ∀ (F E : Type v) [Field F] [Field E] [Algebra F E] (q : ℕ) [ExpChar F q]
      [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ n, finrank F E = q ^ n by
    simpa using this (⊥ : IntermediateField F E) E q
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q : ℕ
inst_3 : ExpChar F_1 q
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
F E : Type v
_ :
  ∀ [inst : Field F] [inst_6 : Field E] [inst_7 : Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E]
    [FiniteDimensional F E], ∃ (n : ℕ), finrank F E = q ^ n
⊢ ∀ [inst : Field F] [inst_6 : Field E] [inst_7 : Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E]
    [FiniteDimensional F E], ∃ (n : ℕ), finrank F E = q ^ n

Tactic:
_
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q : ℕ
inst_3 : ExpChar F_1 q
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
F E : Type v
inst_6 : Field F
_ :
  ∀ [inst : Field E] [inst_7 : Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E],
    ∃ (n : ℕ), finrank F E = q ^ n
⊢ ∀ [inst : Field E] [inst_7 : Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E],
    ∃ (n : ℕ), finrank F E = q ^ n

Tactic:
_
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q : ℕ
inst_3 : ExpChar F_1 q
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
F E : Type v
inst_6 : Field F
inst_7 : Field E
_ :
  ∀ [inst : Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E],
    ∃ (n : ℕ), finrank F E = q ^ n
⊢ ∀ [inst : Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E],
    ∃ (n : ℕ), finrank F E = q ^ n

Tactic:
_
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F_1 : Type u
E_1 : Type v
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
q_1 : ℕ
inst_3 : ExpChar F_1 q_1
inst_4 : IsPurelyInseparable F_1 E_1
inst_5 : FiniteDimensional F_1 E_1
F E : Type v
inst_6 : Field F
inst_7 : Field E
inst_8 : Algebra F E
q : ℕ
_ : ∀ [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ (n : ℕ), finrank F E = q ^ n
⊢ ∀ [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ (n : ℕ), finrank F E = q ^ n

Tactic:
_