awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst_3 : Algebra.IsSeparable F E
h : ∀ (s : Finset ι), LinearIndependent (ι := ↥s) F (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))
s : Finset ι
E' : IntermediateField F E := adjoin F (↑(Finset.image v s) : Set E)
this : FiniteDimensional.{u, v} F ↥E'
v' : (i : ↥s) → ↥E' := fun (i : ↥s) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ E') (v (↑i : ι)) ⋯
h' : LinearIndependent F v'
⊢ LinearIndependent.{u_1, u, v} (ι := ↥s) F (M := E)
    ((fun (x : ι) ↦ v x ^ q ^ n) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))

Tactic:
(h'.map_pow_expChar_pow_of_fd_isSeparable q n).map'
    E'.val.toLinearMap (LinearMap.ker_eq_bot_of_injective E'.val.injective)

Premises used: AlgHom.toLinearMap, _private.0.LinearIndependent.map_pow_expChar_pow_of_fd_isSeparable, LinearIndependent.map', RingHom.injective, AlgHom.toRingHom, LinearMap.ker_eq_bot_of_injective, IntermediateField.val
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst_3 : Algebra.IsSeparable F E
h : ∀ (s : Finset ι), LinearIndependent (ι := ↥s) F (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))
s : Finset ι
E' : IntermediateField F E := adjoin F (↑(Finset.image v s) : Set E)
this : FiniteDimensional.{u, v} F ↥E'
v' : (i : ↥s) → ↥E' := fun (i : ↥s) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ E') (v (↑i : ι)) ⋯
h' : LinearIndependent F v'
⊢ LinearIndependent.{u_1, u, v} (ι := ↥s) F (M := E)
    ((fun (x : ι) ↦ v x ^ q ^ n) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))

Tactic:
exact (h'.map_pow_expChar_pow_of_fd_isSeparable q n).map'
    E'.val.toLinearMap (LinearMap.ker_eq_bot_of_injective E'.val.injective)

Premises used: AlgHom.toLinearMap, _private.0.LinearIndependent.map_pow_expChar_pow_of_fd_isSeparable, LinearIndependent.map', RingHom.injective, AlgHom.toRingHom, LinearMap.ker_eq_bot_of_injective, IntermediateField.val
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst_3 : Algebra.IsSeparable F E
h : LinearIndependent F v
rw rw₁ rw₂ rw₃ :
  ∀ (h : ∀ (s : Finset ι), LinearIndependent (ι := ↥s) F (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))) (s : Finset ι),
    LinearIndependent.{u_1, u, v} (ι := ↥s) F (M := E)
      ((fun (x : ι) ↦ v x ^ q ^ n) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))
rw₄ :
  ∀ (h : ∀ (s : Finset ι), LinearIndependent (ι := ↥s) F (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))) (s : Finset ι),
    LinearIndependent.{u_1, u, v} (ι := ↥s) F (M := E)
      ((fun (x : ι) ↦ v x ^ q ^ n) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))
rw₅ rw₆ :
  ∀ (h : ∀ (s : Finset ι), LinearIndependent (ι := ↥s) F (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))) (s : Finset ι),
    let E' : IntermediateField F E := adjoin F (↑(Finset.image v s) : Set E);
    ∀ (this : FiniteDimensional.{u, v} F ↥E'),
      LinearIndependent.{u_1, u, v} (ι := ↥s) F (M := E)
        ((fun (x : ι) ↦ v x ^ q ^ n) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))
rw₇ :
  ∀ (h : ∀ (s : Finset ι), LinearIndependent (ι := ↥s) F (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))) (s : Finset ι),
    let E' : IntermediateField F E := adjoin F (↑(Finset.image v s) : Set E);
    ∀ (this : FiniteDimensional.{u, v} F ↥E'),
      let v' : (i : ↥s) → ↥E' := fun (i : ↥s) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ E') (v (↑i : ι)) ⋯;
      ∀ (h' : LinearIndependent F v'),
        LinearIndependent.{u_1, u, v} (ι := ↥s) F (M := E)
          ((fun (x : ι) ↦ v x ^ q ^ n) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))
⊢ LinearIndependent.{u_1, u, v} F (M := E) fun (x : ι) ↦ v x ^ q ^ n

Tactic:
classical
  rw [linearIndependent_iff_finset_linearIndependent] at h ⊢
  intro s
  let E' := adjoin F (s.image v : Set E)
  haveI : FiniteDimensional F E' := finiteDimensional_adjoin
    fun x _ ↦ Algebra.IsIntegral.isIntegral x
  let v' (i : s) : E' := ⟨v i.1, subset_adjoin F _ (Finset.mem_image.2 ⟨i.1, i.2, rfl⟩)⟩
  have h' : LinearIndependent F v' := (h s).of_comp E'.val.toLinearMap
  exact (h'.map_pow_expChar_pow_of_fd_isSeparable q n).map'
    E'.val.toLinearMap (LinearMap.ker_eq_bot_of_injective E'.val.injective)

Premises used: linearIndependent_iff_finset_linearIndependent
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : 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)
y : ι
⊢ IsSeparable F (v y)

Tactic:
hsep y
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : 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)
y : ι
⊢ IsSeparable F (v y)

Tactic:
exact hsep y
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : 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)
⊢ Algebra.IsSeparable.{u, v} F ↥E'

Tactic:
haveI : Algebra.IsSeparable F E' := (isSeparable_adjoin_iff_isSeparable F _).2 <| by
    rintro _ ⟨y, rfl⟩; exact hsep y
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : 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)
this : Algebra.IsSeparable.{u, v} F ↥E'
v' : (i : ι) → ↥E' := fun (i : ι) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ E') (v i) ⋯
⊢ LinearIndependent F v'

Tactic:
have h' : LinearIndependent F v' := h.of_comp E'.val.toLinearMap
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : 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)
this : Algebra.IsSeparable.{u, v} F ↥E'
v' : (i : ι) → ↥E' := fun (i : ι) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ E') (v i) ⋯
h' : LinearIndependent F v'
⊢ LinearIndependent.{u_1, u, v} F (M := E) fun (x : ι) ↦ v x ^ q ^ n

Tactic:
(h'.map_pow_expChar_pow_of_isSeparable q n).map'
    E'.val.toLinearMap (LinearMap.ker_eq_bot_of_injective E'.val.injective)

Premises used: AlgHom.toLinearMap, LinearIndependent.map', RingHom.injective, AlgHom.toRingHom, LinearIndependent.map_pow_expChar_pow_of_isSeparable, LinearMap.ker_eq_bot_of_injective, IntermediateField.val
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : 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)
this : Algebra.IsSeparable.{u, v} F ↥E'
v' : (i : ι) → ↥E' := fun (i : ι) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ E') (v i) ⋯
h' : LinearIndependent F v'
⊢ LinearIndependent.{u_1, u, v} F (M := E) fun (x : ι) ↦ v x ^ q ^ n

Tactic:
exact (h'.map_pow_expChar_pow_of_isSeparable q n).map'
    E'.val.toLinearMap (LinearMap.ker_eq_bot_of_injective E'.val.injective)

Premises used: AlgHom.toLinearMap, LinearIndependent.map', RingHom.injective, AlgHom.toRingHom, LinearIndependent.map_pow_expChar_pow_of_isSeparable, LinearMap.ker_eq_bot_of_injective, IntermediateField.val
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
hF : ExpChar F q
inst_3 : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
⊢ IsIntegral F a

Tactic:
have hai : IsIntegral F a := hsep.isIntegral
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
hF : ExpChar F q
inst_3 : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
⊢ IsIntegral F (A := E) ((iterateFrobenius E q n : (a : E) → E) a : E)

Tactic:
have hapi : IsIntegral F (iterateFrobenius E q n a) := hai.pow _
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
hF : ExpChar F q
inst_3 : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
hapi : IsIntegral F (A := E) ((iterateFrobenius E q n : (a : E) → E) a : E)
symm :
  Eq (α := Polynomial F) (Polynomial.map (iterateFrobenius F q n) (minpoly F a))
    (minpoly F (B := E) ((iterateFrobenius E q n : (a : E) → E) a : E))
⊢ Eq (α := Polynomial F) (minpoly F (B := E) ((iterateFrobenius E q n : (a : E) → E) a : E))
    (Polynomial.map (iterateFrobenius F q n) (minpoly F a))

Tactic:
symm
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
hF : ExpChar F q
inst_3 : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
hapi : IsIntegral F (A := E) ((iterateFrobenius E q n : (a : E) → E) a : E)
⊢ Eq (α := Polynomial F) (Polynomial.map (iterateFrobenius F q n) (minpoly F a))
    (minpoly F (B := E) ((iterateFrobenius E q n : (a : E) → E) a : E))

Tactic:
Polynomial.eq_of_monic_of_dvd_of_natDegree_le
    (minpoly.monic hapi)
    (minpoly.monic hai |>.map _)
    (minpoly.dvd F (a ^ q ^ n) ?haeval)
    ?hdeg

Premises used: minpoly.monic, Polynomial.eq_of_monic_of_dvd_of_natDegree_le, HPow.hPow, minpoly.dvd, Polynomial.Monic.map
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
hF : ExpChar F q
inst_3 : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
hapi : IsIntegral F (A := E) ((iterateFrobenius E q n : (a : E) → E) a : E)
haeval :
  Eq.{v + 1} (α := E)
    ((Polynomial.aeval (a ^ q ^ n) : (a : Polynomial F) → E) (Polynomial.map (iterateFrobenius F q n) (minpoly F a)) :
      E)
    (0 : E)
hdeg :
  Polynomial.natDegree (Polynomial.map (iterateFrobenius F q n) (minpoly F a)) ≤
    Polynomial.natDegree (minpoly F (B := E) ((iterateFrobenius E q n : (a : E) → E) a : E))
⊢ Eq (α := Polynomial F) (Polynomial.map (iterateFrobenius F q n) (minpoly F a))
    (minpoly F (B := E) ((iterateFrobenius E q n : (a : E) → E) a : E))

Tactic:
refine Polynomial.eq_of_monic_of_dvd_of_natDegree_le
    (minpoly.monic hapi)
    (minpoly.monic hai |>.map _)
    (minpoly.dvd F (a ^ q ^ n) ?haeval)
    ?hdeg
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
hF : ExpChar F q
inst_3 : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
hapi : IsIntegral F (A := E) ((iterateFrobenius E q n : (a : E) → E) a : E)
⊢ Eq.{v + 1} (α := E)
    ((Polynomial.aeval (a ^ q ^ n) : (a : Polynomial F) → E) (Polynomial.map (iterateFrobenius F q n) (minpoly F a)) :
      E)
    (0 : E)

Tactic:
simpa using Eq.symm <|
      (minpoly F a).map_aeval_eq_aeval_map (RingHom.iterateFrobenius_comm _ q n) a

Premises used: minpoly, Eq.symm, RingHom.iterateFrobenius_comm, Polynomial.map_aeval_eq_aeval_map
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
hF : ExpChar F q
inst_3 : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
hapi : IsIntegral F (A := E) ((iterateFrobenius E q n : (a : E) → E) a : E)
hdeg :
  Polynomial.natDegree (minpoly F a) ≤
    Polynomial.natDegree (minpoly F (B := E) ((iterateFrobenius E q n : (a : E) → E) a : E))
hdeg₁ :
  finrank.{u, v} F ↥F⟮a⟯ ≤ Polynomial.natDegree (minpoly F (B := E) ((iterateFrobenius E q n : (a : E) → E) a : E))
hdeg₂ :
  finrank.{u, v} F ↥F⟮a ^ q ^ n⟯ ≤
    Polynomial.natDegree (minpoly F (B := E) ((iterateFrobenius E q n : (a : E) → E) a : E))
hdeg₃ : finrank.{u, v} F ↥F⟮a ^ q ^ n⟯ ≤ finrank.{u, v} F ↥F⟮((iterateFrobenius E q n : (a : E) → E) a : E)⟯
hdeg₄ hdeg₅ : finrank.{u, v} F ↥F⟮a ^ q ^ n⟯ ≤ finrank.{u, v} F ↥F⟮a ^ q ^ n⟯
⊢ Polynomial.natDegree (Polynomial.map (iterateFrobenius F q n) (minpoly F a)) ≤
    Polynomial.natDegree (minpoly F (B := E) ((iterateFrobenius E q n : (a : E) → E) a : E))

Tactic:
rw [(minpoly F a).natDegree_map_eq_of_injective (iterateFrobenius F q n).injective,
      ← IntermediateField.adjoin.finrank hai,
      IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable F E hsep q n,
      ← IntermediateField.adjoin.finrank hapi, iterateFrobenius_def]

Premises used: IntermediateField.adjoin.finrank, RingHom.injective, iterateFrobenius_def, minpoly, iterateFrobenius, Polynomial.natDegree_map_eq_of_injective, IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
hF : ExpChar F q
inst_3 : ExpChar E q
a : E
hsep : IsSeparable F a
⊢ Eq (α := Polynomial F) (minpoly F (B := E) ((frobenius E q : (a : E) → E) a : E))
    (Polynomial.map (frobenius F q) (minpoly F a))

Tactic:
simpa using minpoly.iterateFrobenius_of_isSeparable q 1 hsep

Premises used: minpoly.iterateFrobenius_of_isSeparable, OfNat.ofNat
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
⊢ ExpChar E p

Tactic:
haveI := expChar_of_injective_algebraMap (algebraMap F E).injective p
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
x : F
obtain :
  ∀ (y : E) (h : Eq (α := E) ((frobenius E p : (a : E) → E) y : E) ((algebraMap F E : (a : F) → E) x : E)),
    ∃ (a : F), (frobenius F p : (a : F) → F) a = x
⊢ ∃ (a : F), (frobenius F p : (a : F) → F) a = x

Tactic:
obtain ⟨y, h⟩ := surjective_frobenius E p (algebraMap F E x)

Premises used: Algebra.algebraMap, surjective_frobenius, DFunLike.coe
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h_1 : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
x : F
y : E
h : Eq (α := E) ((frobenius E p : (a : E) → E) y : E) ((algebraMap F E : (a : F) → E) x : E)
rw : (frobenius E p : (a : E) → E) y = y ^ HPow.hPow (β := ℕ) (ringExpChar F) 1
rw₁ : (frobenius E p : (a : E) → E) y = y ^ ringExpChar F
rw₂ : y ^ p = y ^ ringExpChar F
rw₃ rw₄ : y ^ p = y ^ p
⊢ (algebraMap F E : (a : F) → E) x = y ^ HPow.hPow (β := ℕ) (ringExpChar F) 1

Tactic:
rw [← h, pow_one, frobenius_def, ringExpChar.eq F p]

Premises used: ringExpChar.eq, frobenius_def, pow_one
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h_1 : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
x : F
y : E
h : Eq (α := E) ((frobenius E p : (a : E) → E) y : E) ((algebraMap F E : (a : F) → E) x : E)
⊢ Membership.mem (γ := IntermediateField F E) (perfectClosure F E) y

Tactic:
have : y ∈ perfectClosure F E := ⟨1, x, by rw [← h, pow_one, frobenius_def, ringExpChar.eq F p]⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h_1 : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this_1 : ExpChar E p
x : F
y : E
h : Eq (α := E) ((frobenius E p : (a : E) → E) y : E) ((algebraMap F E : (a : F) → E) x : E)
this : Membership.mem (γ := IntermediateField F E) (perfectClosure F E) y
obtain :
  ∀ (z : F)
    (h :
      Eq (α := E) ((frobenius E p : (a : E) → E) ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z : E) : E)
        ((algebraMap F E : (a : F) → E) x : E))
    (this :
      Membership.mem (α := E) (γ := IntermediateField F E) (perfectClosure F E)
        ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z : E)),
    ∃ (a : F), (frobenius F p : (a : F) → F) a = x
⊢ ∃ (a : F), (frobenius F p : (a : F) → F) a = x

Tactic:
obtain ⟨z, rfl⟩ := eq ▸ this

Premises used: rfl
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h_1 : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this_1 : ExpChar E p
x z : F
h :
  Eq (α := E) ((frobenius E p : (a : E) → E) ((algebraMap F E : (a : F) → E) z : E) : E)
    ((algebraMap F E : (a : F) → E) x : E)
this :
  Membership.mem (α := E) (γ := IntermediateField F E) (perfectClosure F E)
    ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z : E)
rw :
  Eq (α := E) ((frobenius E p : (a : E) → E) ((algebraMap F E : (a : F) → E) z : E) : E)
    (((algebraMap F E : F →+* E) : (a : F) → E) x : E)
⊢ Eq.{v + 1} (α := E) (((algebraMap F E : F →+* E) : (a : F) → E) ((frobenius F p : (a : F) → F) z : F) : E)
    (((algebraMap F E : F →+* E) : (a : F) → E) x : E)

Tactic:
rw [RingHom.map_frobenius]

Premises used: RingHom.map_frobenius
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h_1 : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this_1 : ExpChar E p
x z : F
h :
  Eq (α := E) ((frobenius E p : (a : E) → E) ((algebraMap F E : (a : F) → E) z : E) : E)
    ((algebraMap F E : (a : F) → E) x : E)
this :
  Membership.mem (α := E) (γ := IntermediateField F E) (perfectClosure F E)
    ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z : E)
rw rw₁ : Eq.{v + 1} (α := E) ((algebraMap F E : (a : F) → E) x : E) (((algebraMap F E : F →+* E) : (a : F) → E) x : E)
⊢ Eq (α := E) ((frobenius E p : (a : E) → E) ((algebraMap F E : (a : F) → E) z : E) : E)
    (((algebraMap F E : F →+* E) : (a : F) → E) x : E)

Tactic:
rw [h]
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h_1 : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this_1 : ExpChar E p
x z : F
h :
  Eq (α := E) ((frobenius E p : (a : E) → E) ((algebraMap F E : (a : F) → E) z : E) : E)
    ((algebraMap F E : (a : F) → E) x : E)
this :
  Membership.mem (α := E) (γ := IntermediateField F E) (perfectClosure F E)
    ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z : E)
⊢ ∃ (a : F), (frobenius F p : (a : F) → F) a = x

Tactic:
exact ⟨z, (algebraMap F E).injective (by rw [RingHom.map_frobenius]; rw [h])⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
⊢ PerfectRing F p

Tactic:
haveI := PerfectRing.ofSurjective F p fun x ↦ by
    obtain ⟨y, h⟩ := surjective_frobenius E p (algebraMap F E x)
    have : y ∈ perfectClosure F E := ⟨1, x, by rw [← h, pow_one, frobenius_def, ringExpChar.eq F p]⟩
    obtain ⟨z, rfl⟩ := eq ▸ this
    simp only [Algebra.ofId] at h
    exact ⟨z, (algebraMap F E).injective (by rw [RingHom.map_frobenius]; rw [h])⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this_1 : ExpChar E p
this : PerfectRing F p
⊢ PerfectField F

Tactic:
PerfectRing.toPerfectField F p

Premises used: PerfectRing.toPerfectField
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this_1 : ExpChar E p
this : PerfectRing F p
⊢ PerfectField F

Tactic:
exact PerfectRing.toPerfectField F p

Premises used: PerfectRing.toPerfectField
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
inst_4 : PerfectField E
⊢ PerfectField F

Tactic:
perfectField_of_perfectClosure_eq_bot F E (perfectClosure.eq_bot_of_isSeparable F E)

Premises used: perfectField_of_perfectClosure_eq_bot, perfectClosure.eq_bot_of_isSeparable
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsAlgClosure F E
⊢ PerfectField F ↔ Algebra.IsSeparable F E

Tactic:
⟨fun _ ↦ IsSepClosure.separable, fun _ ↦ haveI : IsAlgClosed E := IsAlgClosure.isAlgClosed F
    perfectField_of_isSeparable_of_perfectField_top F E⟩

Premises used: perfectField_of_isSeparable_of_perfectField_top, Iff.intro, IsSepClosure.separable
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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 E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
obtain : ∀ (q : ℕ), ExpChar F q → LinearIndependent E v
⊢ LinearIndependent E v

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

Premises used: ExpChar.exists
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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 E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
⊢ ExpChar K q

Tactic:
haveI := expChar_of_injective_algebraMap (algebraMap F K).injective q
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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 E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this : ExpChar K q
⊢ LinearIndependent E v

Tactic:
linearIndependent_iff.mpr fun l hl ↦ Finsupp.ext fun i ↦ ?_

Premises used: Iff.mpr, Finsupp.ext, linearIndependent_iff
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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 E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this : ExpChar K q
refine :
  ∀ (l : ι →₀ E) (hl : Eq.{w + 1} (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (0 : K)) (i : ι),
    Eq.{v + 1} (α := E) ((l : (a : ι) → E) i : E) ((0 : (a : ι) → E) i : E)
⊢ LinearIndependent E v

Tactic:
refine linearIndependent_iff.mpr fun l hl ↦ Finsupp.ext fun i ↦ ?_

Premises used: Iff.mpr, Finsupp.ext, linearIndependent_iff