awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
h_1 : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x : R
y : K
n : ℕ
a : k
ha : ((algebraMap k K : k →+* K) : (a : k) → K) a = y ^ q ^ n
this : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n))
h :
  Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
    (HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n)))
⊢ Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
    (HPow.hPow (α := R ⊗[k] K) (x ⊗ₜ[k] y) (q ^ n))

Tactic:
rw [Algebra.TensorProduct.tmul_pow, this]

Premises used: Algebra.TensorProduct.tmul_pow
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
h : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x : R
y : K
n : ℕ
a : k
ha : ((algebraMap k K : k →+* K) : (a : k) → K) a = y ^ q ^ n
this : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n))
⊢ Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
    (HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n)))

Tactic:
Subring.mul_mem _ ⟨x ^ q ^ n, rfl⟩ ⟨algebraMap k R a, ?_⟩

Premises used: Algebra.algebraMap, Set.Mem, HPow.hPow, Exists.intro, Subring.mul_mem, DFunLike.coe, rfl
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
h_1 : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x : R
y : K
n : ℕ
a : k
ha : ((algebraMap k K : k →+* K) : (a : k) → K) a = y ^ q ^ n
this : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n))
h :
  Eq (α := R ⊗[k] K)
    (((algebraMap R (R ⊗[k] K) : R →+* R ⊗[k] K) : (a : R) → R ⊗[k] K) ((algebraMap k R : (a : k) → R) a) : R ⊗[k] K)
    (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
⊢ Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
    (HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n)))

Tactic:
refine Subring.mul_mem _ ⟨x ^ q ^ n, rfl⟩ ⟨algebraMap k R a, ?_⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
h_1 : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x : R
y : K
n : ℕ
a : k
ha : ((algebraMap k K : k →+* K) : (a : k) → K) a = y ^ q ^ n
this : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n))
h : Eq (α := R ⊗[k] K) ((algebraMap k (R ⊗[k] K) : (a : k) → R ⊗[k] K) a : R ⊗[k] K) (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
h₁ : Eq (α := R ⊗[k] K) ((algebraMap k R : (a : k) → R) a ⊗ₜ[k] 1 : R ⊗[k] K) (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
h₂ : Eq (α := R ⊗[k] K) (1 ⊗ₜ[k] (algebraMap k K : (a : k) → K) a : R ⊗[k] K) (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
h₃ h₄ : Eq (α := R ⊗[k] K) (1 ⊗ₜ[k] (y ^ q ^ n)) (1 ⊗ₜ[k] (y ^ q ^ n))
⊢ Eq (α := R ⊗[k] K)
    (((algebraMap R (R ⊗[k] K) : R →+* R ⊗[k] K) : (a : R) → R ⊗[k] K) ((algebraMap k R : (a : k) → R) a) : R ⊗[k] K)
    (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)

Tactic:
rw [← IsScalarTower.algebraMap_apply, Algebra.TensorProduct.algebraMap_apply,
      Algebra.TensorProduct.tmul_one_eq_one_tmul, ha]

Premises used: Algebra.TensorProduct.algebraMap_apply, Algebra.TensorProduct.tmul_one_eq_one_tmul, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
x : R ⊗[k] K
h : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)

Tactic:
induction x with
  | zero => exact ⟨0, 0, by simp⟩
  | add x y h h' =>
    have : ExpChar (R ⊗[k] K) q := expChar_of_injective_ringHom (algebraMap k _).injective q
    simp_rw [RingHom.mem_range, ← RingHom.mem_rangeS, ← Subalgebra.mem_perfectClosure_iff] at h h' ⊢
    exact add_mem h h'
  | tmul x y =>
    obtain ⟨n, a, ha⟩ := IsPurelyInseparable.pow_mem k q y
    use n
    have : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) =
        (x ^ q ^ n) ⊗ₜ[k] (1 : K) * (1 : R) ⊗ₜ[k] (y ^ q ^ n) := by
      rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
    rw [Algebra.TensorProduct.tmul_pow, this]
    refine Subring.mul_mem _ ⟨x ^ q ^ n, rfl⟩ ⟨algebraMap k R a, ?_⟩
    rw [← IsScalarTower.algebraMap_apply, Algebra.TensorProduct.algebraMap_apply,
      Algebra.TensorProduct.tmul_one_eq_one_tmul, ha]

Premises used: Algebra.TensorProduct.algebraMap_apply, RingHom.mem_range, RingHom.mem_rangeS, Algebra.TensorProduct.tmul_pow, Algebra.TensorProduct.tmul_one_eq_one_tmul, TensorProduct.tmul, Subalgebra.mem_perfectClosure_iff, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
x : R ⊗[k] K
h : Nontrivial (R ⊗[k] K)
hq : q = 1
inr :
  ∀ [ExpChar k 1],
    ∃ (n : ℕ),
      Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
        (x ^ HPow.hPow (α := ℕ) 1 n)
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)

Tactic:
subst hq
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
x : R ⊗[k] K
h : Nontrivial (R ⊗[k] K)
inst_6 : ExpChar k 1
⊢ CharZero k

Tactic:
have : CharZero k := charZero_of_expChar_one' k
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
x : R ⊗[k] K
h : Nontrivial (R ⊗[k] K)
inst_6 : ExpChar k 1
this : CharZero k
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
      (x ^ HPow.hPow (α := ℕ) 1 n)

Tactic:
⟨0, (Algebra.TensorProduct.includeLeft_surjective R _ <|
      IsPurelyInseparable.surjective_algebraMap_of_isSeparable k K) _⟩

Premises used: IsPurelyInseparable.surjective_algebraMap_of_isSeparable, Exists.intro, OfNat.ofNat, Algebra.TensorProduct.includeLeft_surjective
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
x : R ⊗[k] K
h : Nontrivial (R ⊗[k] K)
inst_6 : ExpChar k 1
this : CharZero k
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
      (x ^ HPow.hPow (α := ℕ) 1 n)

Tactic:
exact ⟨0, (Algebra.TensorProduct.includeLeft_surjective R _ <|
      IsPurelyInseparable.surjective_algebraMap_of_isSeparable k K) _⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
x : R ⊗[k] K
q : ℕ := ringExpChar k
obtain :
  ∀ (n : ℕ)
    (hr : Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)),
    ∃ n > 0, Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ n)
⊢ ∃ n > 0, Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ n)

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

Premises used: IsPurelyInseparable.exists_pow_pow_mem_range_tensorProduct_of_expChar
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
x : R ⊗[k] K
q : ℕ := ringExpChar k
n : ℕ
hr : Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
⊢ ∃ n > 0, Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ n)

Tactic:
⟨q ^ n, pow_pos ?_ _, hr⟩

Premises used: pow_pos, HPow.hPow, And.intro, Exists.intro
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
x : R ⊗[k] K
q : ℕ := ringExpChar k
n : ℕ
hr : Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
refine : 0 < q
⊢ ∃ n > 0, Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ n)

Tactic:
refine ⟨q ^ n, pow_pos ?_ _, hr⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
x : R ⊗[k] K
q : ℕ := ringExpChar k
n : ℕ
hr : Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
inl : ∀ (hq : Nat.Prime q), 0 < q
inr : ∀ (hq : q = 1), 0 < q
⊢ 0 < q

Tactic:
obtain (hq | hq) := expChar_is_prime_or_one k q

Premises used: expChar_is_prime_or_one
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
x : R ⊗[k] K
q : ℕ := ringExpChar k
n : ℕ
hr : Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
hq : Nat.Prime q
⊢ 0 < q

Tactic:
simp [hq, Nat.Prime.pos]

Premises used: Nat.Prime.pos
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
x : R ⊗[k] K
q : ℕ := ringExpChar k
n : ℕ
hr : Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
hq : q = 1
⊢ 0 < q

Tactic:
simp [hq, Nat.Prime.pos]

Premises used: Nat.Prime.pos
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : CommRing K
inst_1 : Ring L
inst_2 : Algebra K L
p : ℕ
inst_3 : ExpChar K p
⊢ HasExponent K L ↔
    ∃ (e : ℕ),
      ∀ (a : L), Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ p ^ e)

Tactic:
ringExpChar.eq K p ▸ hasExponent_iff K L

Premises used: ringExpChar.eq, IsPurelyInseparable.hasExponent_iff, Eq.rec
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : CommRing K
inst_1 : Ring L
inst_2 : Algebra K L
inst_3 : HasExponent K L
a : L
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L))
    (a ^ ringExpChar K ^ exponent K L)

Tactic:
Nat.find_spec ‹HasExponent K L›.has_exponent a

Premises used: Set.Mem, IsPurelyInseparable.HasExponent.has_exponent, IsPurelyInseparable.exponent, Nat.find_spec
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : CommRing K
inst_1 : Ring L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
a : L
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ p ^ exponent K L)

Tactic:
ringExpChar.eq K p ▸ exponent_def K a

Premises used: ringExpChar.eq, Eq.rec, IsPurelyInseparable.exponent_def
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : CommRing K
inst_1 : Ring L
inst_2 : Algebra K L
inst_3 : HasExponent K L
e : ℕ
h : e < exponent K L
⊢ ∃ (a : L), a ^ ringExpChar K ^ e ∉ RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)

Tactic:
not_forall.mp <| Nat.find_min ‹HasExponent K L›.has_exponent h

Premises used: IsPurelyInseparable.HasExponent.has_exponent, Nat.find_min, Iff.mp, Classical.not_forall
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : CommRing K
inst_1 : Ring L
inst_2 : Algebra K L
inst_3 : HasExponent K L
p : ℕ
inst_4 : ExpChar K p
e : ℕ
h : e < exponent K L
⊢ ∃ (a : L), a ^ p ^ e ∉ RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)

Tactic:
ringExpChar.eq K p ▸ exponent_min h

Premises used: ringExpChar.eq, Eq.rec, IsPurelyInseparable.exponent_min
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
F : Type u_1
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Ring L
inst_2 : IsDomain L
inst_3 : Algebra K L
inst_4 : HasExponent K L
⊢ IsPurelyInseparable K L

Tactic:
let ⟨n, h⟩ := ‹HasExponent K L›.has_exponent
  (isPurelyInseparable_iff_pow_mem K (ringExpChar K)).mpr fun x ↦ ⟨n, h x⟩

Premises used: Iff.mpr, ringExpChar, IsPurelyInseparable.HasExponent.has_exponent, isPurelyInseparable_iff_pow_mem, Exists.intro, _private.0.IsPurelyInseparable.instOfHasExponent.match_1, IsPurelyInseparable
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) a
apply :
  ∃ (y : K),
    minpoly K a =
      HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (HPow.hPow (β := ℕ) (ringExpChar K) 0))
        ((C : (a : K) → K[X]) y : K[X])
⊢ elemExponent K a = 0

Tactic:
apply (Nat.find_eq_zero _).mpr

Premises used: Iff.mpr, Nat.find_eq_zero
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) a
rw : ∃ (y : K), minpoly K a = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X])
⊢ ∃ (y : K),
    minpoly K a =
      HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (HPow.hPow (β := ℕ) (ringExpChar K) 0))
        ((C : (a : K) → K[X]) y : K[X])

Tactic:
rw [pow_zero, pow_one]

Premises used: pow_zero, pow_one
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) a
obtain :
  ∀ (y : K) (hy : ((algebraMap K L : K →+* L) : (a : K) → L) y = a),
    ∃ (y : K), minpoly K a = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X])
⊢ ∃ (y : K), minpoly K a = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X])

Tactic:
obtain ⟨y, hy⟩ := h
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
y : K
hy : ((algebraMap K L : K →+* L) : (a : K) → L) y = a
⊢ ∃ (y : K), minpoly K a = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X])

Tactic:
⟨y, hy ▸ minpoly.eq_X_sub_C L y⟩

Premises used: Eq.rec, Exists.intro, minpoly.eq_X_sub_C
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
y : K
hy : ((algebraMap K L : K →+* L) : (a : K) → L) y = a
⊢ ∃ (y : K), minpoly K a = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X])

Tactic:
exact ⟨y, hy ▸ minpoly.eq_X_sub_C L y⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
inst_4 : CharZero K
⊢ elemExponent K a = 0

Tactic:
elemExponent_eq_zero_of_mem_range <| surjective_algebraMap_of_isSeparable K L a

Premises used: IsPurelyInseparable.surjective_algebraMap_of_isSeparable, IsPurelyInseparable.elemExponent_eq_zero_of_mem_range
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
⊢ minpoly K a =
    HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
      ((C : (a : K) → K[X]) (elemReduct K a) : K[X])

Tactic:
Classical.choose_spec <| Nat.find_spec <| minpoly_eq_X_pow_sub_C K (ringExpChar K) a

Premises used: ringExpChar, IsPurelyInseparable.elemReduct, Classical.choose_spec, IsPurelyInseparable.elemExponent, IsPurelyInseparable.minpoly_eq_X_pow_sub_C, Nat.find_spec
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
p : ℕ
inst_4 : ExpChar K p
a : L
⊢ minpoly K a =
    HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (p ^ elemExponent K a))
      ((C : (a : K) → K[X]) (elemReduct K a) : K[X])

Tactic:
ringExpChar.eq K p ▸ minpoly_eq K a

Premises used: ringExpChar.eq, IsPurelyInseparable.minpoly_eq, Eq.rec
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
rw :
  (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
        ((C : (a : K) → K[X]) (elemReduct K a) : K[X])).natDegree =
    ringExpChar K ^ elemExponent K a
rw₁ : (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)).natDegree = ringExpChar K ^ elemExponent K a
rw₂ : ringExpChar K ^ elemExponent K a * natDegree.{u_2} (R := K) X = ringExpChar K ^ elemExponent K a
rw₃ : ringExpChar K ^ elemExponent K a * 1 = ringExpChar K ^ elemExponent K a
rw₄ rw₅ : ringExpChar K ^ elemExponent K a = ringExpChar K ^ elemExponent K a
⊢ natDegree (minpoly K a) = ringExpChar K ^ elemExponent K a

Tactic:
rw [minpoly_eq K a, natDegree_sub_C, natDegree_pow, natDegree_X, mul_one]

Premises used: Polynomial.natDegree_X, IsPurelyInseparable.minpoly_eq, Polynomial.natDegree_pow, Polynomial.natDegree_sub_C, mul_one
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
p : ℕ
inst_4 : ExpChar K p
a : L
⊢ natDegree (minpoly K a) = p ^ elemExponent K a

Tactic:
ringExpChar.eq K p ▸ minpoly_natDegree_eq K a

Premises used: ringExpChar.eq, Eq.rec, IsPurelyInseparable.minpoly_natDegree_eq
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
⊢ Eq.{u_3 + 1} (α := L)
    ((aeval a : (a : K[X]) → L)
        (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
          ((C : (a : K) → K[X]) (elemReduct K a) : K[X])) :
      L)
    (0 : L)

Tactic:
have := minpoly_eq K a ▸ minpoly.aeval K a
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
this :
  Eq.{u_3 + 1} (α := L)
    ((aeval a : (a : K[X]) → L)
        (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
          ((C : (a : K) → K[X]) (elemReduct K a) : K[X])) :
      L)
    (0 : L)
rwa :
  ∀
    (this :
      HSub.hSub (α := L) (β := L)
          ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)) : L)
          ((aeval a : (a : K[X]) → L) ((C : (a : K) → K[X]) (elemReduct K a) : K[X]) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
rwa₁ :
  ∀
    (this :
      HSub.hSub (α := L) (β := L)
          ((aeval a : (a : K[X]) → L) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)) : L)
          ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
rwa₂ :
  ∀
    (this :
      HSub.hSub (β := L) (HPow.hPow (α := L) ((aeval a : (a : K[X]) → L) X : L) (ringExpChar K ^ elemExponent K a))
          ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
rwa₃ :
  ∀
    (this :
      HSub.hSub (β := L) (a ^ ringExpChar K ^ elemExponent K a) ((algebraMap K L : (a : K) → L) (elemReduct K a) : L) =
        0),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
rwa₄ :
  ∀ (this : a ^ ringExpChar K ^ elemExponent K a = (algebraMap K L : (a : K) → L) (elemReduct K a)),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
rwa₅ rwa₆ rwa₇ rwa₈ :
  ∀ (this : (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a),
    (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
⊢ (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a

Tactic:
rwa [map_sub, aeval_C, map_pow, aeval_X, sub_eq_zero, eq_comm] at this

Premises used: map_sub, sub_eq_zero, map_pow, eq_comm, Polynomial.aeval_C, Polynomial.aeval_X
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
p : ℕ
inst_4 : ExpChar K p
a : L
⊢ (algebraMap K L : (a : K) → L) (elemReduct K a) = a ^ p ^ elemExponent K a

Tactic:
ringExpChar.eq K p ▸ algebraMap_elemReduct_eq K a

Premises used: ringExpChar.eq, Eq.rec, IsPurelyInseparable.algebraMap_elemReduct_eq
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L))
    (a ^ ringExpChar K ^ elemExponent K a)

Tactic:
RingHom.mem_range.mpr <| ⟨_, algebraMap_elemReduct_eq K a⟩

Premises used: Iff.mpr, RingHom.mem_range, Exists.intro, IsPurelyInseparable.algebraMap_elemReduct_eq
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
p : ℕ
inst_4 : ExpChar K p
a : L
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ p ^ elemExponent K a)

Tactic:
ringExpChar.eq K p ▸ elemExponent_def K a

Premises used: ringExpChar.eq, Eq.rec, IsPurelyInseparable.elemExponent_def
-- Module: Mathlib.FieldTheory.PurelyInseparable.Exponent
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
n : ℕ
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) (a ^ ringExpChar K ^ n)
let : ∀ (p : ℕ), ExpChar K p → elemExponent K a ≤ n
⊢ elemExponent K a ≤ n

Tactic:
let ⟨p, _⟩ := ExpChar.exists K