awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
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 : Eq (α := Submodule F E) (Submodule.span F (Set.range v)) ⊤
this :
  Eq (α := Submonoid E) (Submonoid.closure (Set.range fun (x : E) ↦ x ^ q ^ n))
    (Submonoid.copy (Submonoid.map (F := E →* E) { toFun := fun (x : E) ↦ x ^ q ^ n, map_one' := ⋯, map_mul' := ⋯ } ⊤)
      (Set.range fun (x : E) ↦ x ^ q ^ n) ⋯)
⊢ Set.range (ι := E) ((Semiring.toMonoid : Monoid E).5 (q ^ n)) ⊆
    (↑(Submodule.span F (Set.range ((Semiring.toMonoid : Monoid E).5 (q ^ n) ∘ v))) : Set E)
have rw : Set.image (α := E) ((Semiring.toMonoid : Monoid E).5 (q ^ n)) Set.univ ⊆
  (↑(Submodule.span F ((Semiring.toMonoid : Monoid E).5 (q ^ n) '' Set.range v)) : Set E)
Tactic: rw [Set.range_comp, ← Set.image_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (hypothesis)
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 : Eq (α := Submodule F E) (Submodule.span F (Set.range v)) ⊤
this :
  Eq (α := Submonoid E) (Submonoid.closure (Set.range fun (x : E) ↦ x ^ q ^ n))
    (Submonoid.copy (Submonoid.map (F := E →* E) { toFun := fun (x : E) ↦ x ^ q ^ n, map_one' := ⋯, map_mul' := ⋯ } ⊤)
      (Set.range fun (x : E) ↦ x ^ q ^ n) ⋯)
⊢ Set.image (α := E) ((Semiring.toMonoid : Monoid E).5 (q ^ n)) Set.univ ⊆
    (↑(Submodule.span F ((Semiring.toMonoid : Monoid E).5 (q ^ n) '' Set.range v)) : Set E)
have this₁ : ExpChar E q
Tactic: haveI := expChar_of_injective_algebraMap (algebraMap F E).injective q
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (hypothesis)
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 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
h : LinearIndependent F v
⊢ LinearIndependent.{u_1, u, v} F (M := E) fun (x : ι) ↦ v x ^ q ^ n
have h' : LinearIndepOn F id (Set.range v)
Tactic: have h' := h.linearIndepOn_id
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (hypothesis)
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 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
h : LinearIndependent F v
h' : LinearIndepOn F id (Set.range v)
ι' : Set E := LinearIndepOn.extend.{v, v, u} (K := F) (V := E) (v := id) (s := Set.range v) (t := Set.univ) h' ⋯
b : Basis (↑ι' : Type v) F E := Basis.extend (s := Set.range v) h'
this : Fintype (↑ι' : Type v) := FiniteDimensional.fintypeBasisIndex.{u, v, v} (K := F) (V := E) b
⊢ LinearIndependent.{u_1, u, v} F (M := E) fun (x : ι) ↦ v x ^ q ^ n
have H : LinearIndependent F (M := E) fun (x : (↑ι' : Type v)) ↦
  HPow.hPow (α := E) ((b : (a : (↑ι' : Type v)) → E) x : E) (q ^ n)
Tactic: have H := linearIndependent_of_top_le_span_of_card_eq_finrank
    (Field.span_map_pow_expChar_pow_eq_top_of_isSeparable q n b.span_eq).ge
    (Module.finrank_eq_card_basis b).symm
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
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 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
h : LinearIndependent F v
h' : LinearIndepOn F id (Set.range v)
ι' : Set E := LinearIndepOn.extend.{v, v, u} (K := F) (V := E) (v := id) (s := Set.range v) (t := Set.univ) h' ⋯
b : Basis (↑ι' : Type v) F E := Basis.extend (s := Set.range v) h'
this : Fintype (↑ι' : Type v) := FiniteDimensional.fintypeBasisIndex.{u, v, v} (K := F) (V := E) b
H :
  LinearIndependent F (M := E) fun (x : (↑ι' : Type v)) ↦
    HPow.hPow (α := E) ((b : (a : (↑ι' : Type v)) → E) x : E) (q ^ n)
f : (i : ι) → (↑ι' : Type v) := fun (i : ι) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ ι') (v i) ⋯
⊢ LinearIndependent.{u_1, u, v} F (M := E) fun (x : ι) ↦ v x ^ q ^ n
have h₁ : ∀ (x : ι),
  v x ^ q ^ n = ((fun (x : (↑ι' : Type v)) ↦ HPow.hPow (α := E) ((b : (a : (↑ι' : Type v)) → E) x : E) (q ^ n)) ∘ f) x
Tactic: convert! H.comp f fun _ _ heq ↦ h.injective (by simpa only [f, Subtype.mk.injEq] using heq)
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
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 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
h : LinearIndependent F v
h' : LinearIndepOn F id (Set.range v)
ι' : Set E := LinearIndepOn.extend.{v, v, u} (K := F) (V := E) (v := id) (s := Set.range v) (t := Set.univ) h' ⋯
b : Basis (↑ι' : Type v) F E := Basis.extend (s := Set.range v) h'
this : Fintype (↑ι' : Type v) := FiniteDimensional.fintypeBasisIndex.{u, v, v} (K := F) (V := E) b
H :
  LinearIndependent F (M := E) fun (x : (↑ι' : Type v)) ↦
    HPow.hPow (α := E) ((b : (a : (↑ι' : Type v)) → E) x : E) (q ^ n)
f : (i : ι) → (↑ι' : Type v) := fun (i : ι) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ ι') (v i) ⋯
x : ι
⊢ v x ^ q ^ n = ((fun (x : (↑ι' : Type v)) ↦ HPow.hPow (α := E) ((b : (a : (↑ι' : Type v)) → E) x : E) (q ^ n)) ∘ f) x
have h₁ : v x ^ q ^ n = HPow.hPow (α := E) ((Basis.extend (s := Set.range v) h' : (a : (↑ι' : Type v)) → E) (f x) : E) (q ^ n)
Tactic: simp_rw [Function.comp_apply, b]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
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 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
h : LinearIndependent F v
h' : LinearIndepOn F id (Set.range v)
ι' : Set E := LinearIndepOn.extend.{v, v, u} (K := F) (V := E) (v := id) (s := Set.range v) (t := Set.univ) h' ⋯
b : Basis (↑ι' : Type v) F E := Basis.extend (s := Set.range v) h'
this : Fintype (↑ι' : Type v) := FiniteDimensional.fintypeBasisIndex.{u, v, v} (K := F) (V := E) b
H :
  LinearIndependent F (M := E) fun (x : (↑ι' : Type v)) ↦
    HPow.hPow (α := E) ((b : (a : (↑ι' : Type v)) → E) x : E) (q ^ n)
f : (i : ι) → (↑ι' : Type v) := fun (i : ι) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ ι') (v i) ⋯
x : ι
⊢ v x ^ q ^ n = HPow.hPow (α := E) ((Basis.extend (s := Set.range v) h' : (a : (↑ι' : Type v)) → E) (f x) : E) (q ^ n)
have h₁ : v x ^ q ^ n = (↑(f x) : E) ^ q ^ n
Tactic: rw [Basis.extend_apply_self]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
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
⊢ LinearIndependent.{u_1, u, v} F (M := E) fun (x : ι) ↦ v x ^ q ^ n
have 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))
Tactic: rw [linearIndependent_iff_finset_linearIndependent] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (hypothesis)
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)
⊢ LinearIndependent.{u_1, u, v} (ι := ↥s) F (M := E)
    ((fun (x : ι) ↦ v x ^ q ^ n) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))
have this : FiniteDimensional.{u, v} F ↥E'
Tactic: haveI : FiniteDimensional F E' := finiteDimensional_adjoin
    fun x _ ↦ Algebra.IsIntegral.isIntegral x
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (hypothesis)
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 : ι)) ⋯
⊢ LinearIndependent.{u_1, u, v} (ι := ↥s) F (M := E)
    ((fun (x : ι) ↦ v x ^ q ^ n) ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))
have h' : LinearIndependent F v'
Tactic: have h' : LinearIndependent F v' := (h s).of_comp E'.val.toLinearMap
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
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
⊢ LinearIndependent.{u_1, u, v} F (M := E) fun (x : ι) ↦ v x ^ q ^ n
have 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))
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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
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))
⊢ LinearIndependent.{u_1, u, v} F (M := E) fun (x : ι) ↦ v x ^ q ^ n
have 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))
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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
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))
⊢ LinearIndependent.{u_1, u, v} F (M := E) fun (x : ι) ↦ v x ^ q ^ n
have 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 : ι)) sorry;
    ∀ (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: 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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (hypothesis)
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)
⊢ LinearIndependent.{u_1, u, v} F (M := E) fun (x : ι) ↦ v x ^ q ^ n
have this : 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
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (hypothesis)
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.{u_1, u, v} F (M := E) fun (x : ι) ↦ v x ^ q ^ n
have h' : LinearIndependent F v'
Tactic: have h' : LinearIndependent F v' := h.of_comp E'.val.toLinearMap
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (hypothesis)
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
⊢ 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))
have hai : IsIntegral F a
Tactic: have hai : IsIntegral F a := hsep.isIntegral
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (hypothesis)
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
⊢ 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))
have hapi : 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 _
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
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) (minpoly F (B := E) ((iterateFrobenius E q n : (a : E) → E) a : E))
    (Polynomial.map (iterateFrobenius F q n) (minpoly F a))
have 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))
Tactic: symm
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
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))
have 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)
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
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
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)
⊢ 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))
have 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))
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
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
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)
⊢ 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))
have hdeg : Polynomial.natDegree (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]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
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))
⊢ 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))
have hdeg₁ : finrank.{u, v} F ↥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]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
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))
⊢ 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))
have hdeg₂ : finrank.{u, v} F ↥F⟮a ^ q ^ n⟯ ≤
  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]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
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))
⊢ 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))
have hdeg₃ : finrank.{u, v} F ↥F⟮a ^ q ^ n⟯ ≤ finrank.{u, v} F ↥F⟮((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]