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
S : Set E
q : ℕ
inst_3 : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst_4 : Algebra.IsSeparable.{u, v} F ↥L
M : IntermediateField F E := adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S)
y : E
hy : y ∈ S
⊢ (fun (x : E) ↦ x ^ q ^ n) y ∈ (↑L : Set E)

Tactic:
exact pow_mem (subset_adjoin F S hy) _

Premises used: IntermediateField.subset_adjoin, pow_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
q : ℕ
inst_3 : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst_4 : Algebra.IsSeparable.{u, v} F ↥L
M : IntermediateField F E := adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S)
⊢ M ≤ L

Tactic:
have hi : M ≤ L := by
    rw [adjoin_le_iff]
    rintro _ ⟨y, hy, rfl⟩
    exact pow_mem (subset_adjoin F S hy) _
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
q : ℕ
inst_3 : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst_4 : Algebra.IsSeparable.{u, v} F ↥L
M : IntermediateField F E := adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S)
hi : M ≤ L
this : Algebra ↥M ↥L := (inclusion hi).toAlgebra
⊢ Algebra.IsSeparable.{v, v} ↥M ↥(extendScalars hi)

Tactic:
haveI : Algebra.IsSeparable M (extendScalars hi) :=
    Algebra.isSeparable_tower_top_of_isSeparable F M L
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
q : ℕ
inst_3 : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst_4 : Algebra.IsSeparable.{u, v} F ↥L
M : IntermediateField F E := adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S)
hi : M ≤ L
this_1 : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this : Algebra.IsSeparable.{v, v} ↥M ↥(extendScalars hi)
rw : ∀ x ∈ S, ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range (R := ↥M) (algebraMap (↥M) E)) (x ^ q ^ n)
⊢ IsPurelyInseparable.{v, v} ↥M ↥(extendScalars hi)

Tactic:
rw [extendScalars_adjoin hi, isPurelyInseparable_adjoin_iff_pow_mem M _ q]

Premises used: Membership.mem, IntermediateField.extendScalars_adjoin, Subtype, IntermediateField.isPurelyInseparable_adjoin_iff_pow_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
q : ℕ
inst_3 : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst_4 : Algebra.IsSeparable.{u, v} F ↥L
M : IntermediateField F E := adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S)
hi : M ≤ L
this_1 : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this : Algebra.IsSeparable.{v, v} ↥M ↥(extendScalars hi)
⊢ ∀ x ∈ S, ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range (R := ↥M) (algebraMap (↥M) E)) (x ^ q ^ n)

Tactic:
fun x hx ↦ ⟨n, ⟨x ^ q ^ n, subset_adjoin F _ ⟨x, hx, rfl⟩⟩, rfl⟩

Premises used: IntermediateField.subset_adjoin, Subtype.mk, HPow.hPow, And.intro, Exists.intro, Set.image, 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
S : Set E
q : ℕ
inst_3 : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst_4 : Algebra.IsSeparable.{u, v} F ↥L
M : IntermediateField F E := adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S)
hi : M ≤ L
this_1 : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this : Algebra.IsSeparable.{v, v} ↥M ↥(extendScalars hi)
⊢ ∀ x ∈ S, ∃ (n : ℕ), Membership.mem (γ := Subring E) (RingHom.range (R := ↥M) (algebraMap (↥M) E)) (x ^ q ^ n)

Tactic:
exact fun x hx ↦ ⟨n, ⟨x ^ q ^ n, subset_adjoin F _ ⟨x, hx, rfl⟩⟩, 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
S : Set E
q : ℕ
inst_3 : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst_4 : Algebra.IsSeparable.{u, v} F ↥L
M : IntermediateField F E := adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S)
hi : M ≤ L
this_1 : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this : Algebra.IsSeparable.{v, v} ↥M ↥(extendScalars hi)
⊢ IsPurelyInseparable.{v, v} ↥M ↥(extendScalars hi)

Tactic:
haveI : IsPurelyInseparable M (extendScalars hi) := by
    rw [extendScalars_adjoin hi, isPurelyInseparable_adjoin_iff_pow_mem M _ q]
    exact fun x hx ↦ ⟨n, ⟨x ^ q ^ n, subset_adjoin F _ ⟨x, hx, rfl⟩⟩, 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
S : Set E
q : ℕ
inst_3 : ExpChar F q
n : ℕ
L : IntermediateField F E := adjoin F S
inst_4 : Algebra.IsSeparable.{u, v} F ↥L
M : IntermediateField F E := adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S)
hi : M ≤ L
this_1 : Algebra ↥M ↥L := (inclusion hi).toAlgebra
this_2 : Algebra.IsSeparable.{v, v} ↥M ↥(extendScalars hi)
this : IsPurelyInseparable.{v, v} ↥M ↥(extendScalars hi)
⊢ L = M

Tactic:
simpa only [extendScalars_restrictScalars, restrictScalars_bot_eq_self] using congr_arg
    (restrictScalars F) (extendScalars hi).eq_bot_of_isPurelyInseparable_of_isSeparable

Premises used: IntermediateField.restrictScalars, IntermediateField.extendScalars, IntermediateField.restrictScalars_bot_eq_self, congr_arg, IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable, IntermediateField.extendScalars_restrictScalars
-- 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
S : Set E
q : ℕ
inst_4 : ExpChar F q
n : ℕ
⊢ Eq (α := IntermediateField F E) (adjoin F S) (adjoin F ((fun (x : E) ↦ x ^ q ^ n) '' S))

Tactic:
haveI := Algebra.isSeparable_tower_bot_of_isSeparable F (adjoin F S) E
  adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable F E S q n

Premises used: IntermediateField.adjoin_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
S : Set E
inst_3 : Algebra.IsSeparable.{u, v} F ↥(adjoin F S)
q : ℕ
inst_4 : ExpChar F q
⊢ Eq (α := IntermediateField F E) (adjoin F S) (adjoin F ((fun (x : E) ↦ x ^ q) '' S))

Tactic:
pow_one q ▸ adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable F E S q 1

Premises used: IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable, Eq.rec, pow_one, 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
inst_3 : Algebra.IsSeparable F E
S : Set E
q : ℕ
inst_4 : ExpChar F q
⊢ Eq (α := IntermediateField F E) (adjoin F S) (adjoin F ((fun (x : E) ↦ x ^ q) '' S))

Tactic:
pow_one q ▸ adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable' F E S q 1

Premises used: IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable', Eq.rec, pow_one, 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
a : E
ha : IsSeparable F a
q : ℕ
inst_3 : ExpChar F q
n : ℕ
⊢ Algebra.IsSeparable.{u, v} F ↥F⟮a⟯

Tactic:
haveI := (isSeparable_adjoin_simple_iff_isSeparable F E).mpr ha
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
a : E
ha : IsSeparable F a
q : ℕ
inst_3 : ExpChar F q
n : ℕ
this : Algebra.IsSeparable.{u, v} F ↥F⟮a⟯
⊢ Eq (α := IntermediateField F E) F⟮a⟯ F⟮a ^ q ^ n⟯

Tactic:
simpa using adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable F E {a} q n

Premises used: IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable, Singleton.singleton
-- 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
a : E
q : ℕ
inst_4 : ExpChar F q
n : ℕ
⊢ Eq (α := IntermediateField F E) F⟮a⟯ F⟮a ^ q ^ n⟯

Tactic:
simpa using adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable F E {a} q n

Premises used: IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable, Singleton.singleton
-- Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
a : E
ha : IsSeparable F a
q : ℕ
inst_3 : ExpChar F q
⊢ Eq (α := IntermediateField F E) F⟮a⟯ F⟮a ^ q⟯

Tactic:
pow_one q ▸ adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable F E ha q 1

Premises used: Eq.rec, pow_one, IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_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
inst_3 : Algebra.IsSeparable F E
a : E
q : ℕ
inst_4 : ExpChar F q
⊢ Eq (α := IntermediateField F E) F⟮a⟯ F⟮a ^ q⟯

Tactic:
pow_one q ▸ adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable' F E a q 1

Premises used: Eq.rec, IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable', pow_one, 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
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)) ⊤
rw :
  Eq (α := Submodule F E) (Submodule.span F (Set.range fun (x : ι) ↦ v x ^ q ^ n))
    (Submodule.span F (↑(Submonoid.closure (Set.range fun (x : E) ↦ x ^ q ^ n)) : Set E))
⊢ Eq.{v + 1} (α := Submodule F E) (Submodule.span F (Set.range fun (x : ι) ↦ v x ^ q ^ n)) ⊤

Tactic:
rw [← Algebra.top_toSubmodule, ← top_toSubalgebra, ← adjoin_univ,
    adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable' F E _ q n,
    adjoin_toSubalgebra_of_isAlgebraic fun x _ ↦ Algebra.IsAlgebraic.isAlgebraic x,
    Set.image_univ, Algebra.adjoin_eq_span]

Premises used: Algebra.IsAlgebraic.isAlgebraic, Set.image_univ, IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable', IntermediateField.adjoin_univ, Algebra.top_toSubmodule, IntermediateField.top_toSubalgebra, Algebra.adjoin_eq_span, IntermediateField.adjoin_toSubalgebra_of_isAlgebraic
-- 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 : Eq (α := Submodule F E) (Submodule.span F (Set.range v)) ⊤
⊢ Eq (α := Submonoid E) (Submonoid.closure (↑(MonoidHom.mrange (F := E →* E) (powMonoidHom (q ^ n))) : Set E))
    (MonoidHom.mrange (F := E →* E) (powMonoidHom (q ^ n)))

Tactic:
have := (MonoidHom.mrange (powMonoidHom (α := E) (q ^ n))).closure_eq
-- 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 : 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) ⋯)
rw :
  Eq (α := Submodule F E) (Submodule.span F (Set.range fun (x : ι) ↦ v x ^ q ^ n))
    (Submodule.span F
      (↑(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 E))
⊢ Eq (α := Submodule F E) (Submodule.span F (Set.range fun (x : ι) ↦ v x ^ q ^ n))
    (Submodule.span F (↑(Submonoid.closure (Set.range fun (x : E) ↦ x ^ q ^ n)) : Set E))

Tactic:
rw [this]
-- 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 : 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) ⋯)
⊢ Eq (α := Submodule F E) (Submodule.span F (Set.range fun (x : ι) ↦ v x ^ q ^ n))
    (Submodule.span F
      (↑(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 E))

Tactic:
(Submodule.span_mono <| Set.range_comp_subset_range _ _).antisymm (Submodule.span_le.2 ?_)

Premises used: Iff.mpr, Set.range_comp_subset_range, setOf, LE.le.antisymm, Submodule.span_mono, Set.range, Submodule.span_le
-- 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 : 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) ⋯)
refine :
  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)
⊢ Eq (α := Submodule F E) (Submodule.span F (Set.range fun (x : ι) ↦ v x ^ q ^ n))
    (Submodule.span F
      (↑(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 E))

Tactic:
refine (Submodule.span_mono <| Set.range_comp_subset_range _ _).antisymm (Submodule.span_le.2 ?_)

Premises used: Iff.mpr, Set.range_comp_subset_range, LE.le.antisymm, Submodule.span_mono, Submodule.span_le
-- 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 : 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) ⋯)
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)
⊢ 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)

Tactic:
rw [Set.range_comp, ← Set.image_univ]

Premises used: Set.range_comp, Set.image_univ
-- 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 : 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) ⋯)
⊢ ExpChar E q

Tactic:
haveI := expChar_of_injective_algebraMap (algebraMap F E).injective q
-- 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 : Eq (α := Submodule F E) (Submodule.span F (Set.range v)) ⊤
this_1 :
  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) ⋯)
this : ExpChar E q
⊢ 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:
apply h ▸ Submodule.image_span_subset_span (LinearMap.iterateFrobenius F E q n) _
-- 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 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
h : LinearIndependent F v
⊢ LinearIndepOn F id (Set.range v)

Tactic:
have h' := h.linearIndepOn_id
-- 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 : 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 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
-- 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 : 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 x_1 : ι
heq : f x = f x_1
⊢ v x = v x_1

Tactic:
simpa only [f, Subtype.mk.injEq] using heq

Premises used: Subtype.mk.injEq
-- 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 : 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) ⋯
h₁ :
  ∀ (x : ι),
    v x ^ q ^ n = ((fun (x : (↑ι' : Type v)) ↦ HPow.hPow (α := E) ((b : (a : (↑ι' : Type v)) → E) x : E) (q ^ n)) ∘ f) x
⊢ LinearIndependent.{u_1, u, v} F (M := E) fun (x : ι) ↦ v x ^ q ^ n

Tactic:
convert! H.comp f fun _ _ heq ↦ h.injective (by simpa only [f, Subtype.mk.injEq] using heq)

Premises used: LinearIndependent.injective, LinearIndependent.comp
-- 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 : 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 : ι
h₁ :
  v x ^ q ^ n = HPow.hPow (α := E) ((Basis.extend (s := Set.range v) h' : (a : (↑ι' : Type v)) → E) (f x) : E) (q ^ n)
⊢ v x ^ q ^ n = ((fun (x : (↑ι' : Type v)) ↦ HPow.hPow (α := E) ((b : (a : (↑ι' : Type v)) → E) x : E) (q ^ n)) ∘ f) x

Tactic:
simp_rw [Function.comp_apply, b]

Premises used: Function.comp_apply
-- 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 : 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 : ι
h₁ h₂ : v x ^ q ^ n = (↑(f x) : E) ^ q ^ n
⊢ v x ^ q ^ n = HPow.hPow (α := E) ((Basis.extend (s := Set.range v) h' : (a : (↑ι' : Type v)) → E) (f x) : E) (q ^ n)

Tactic:
rw [Basis.extend_apply_self]

Premises used: Module.Basis.extend_apply_self
-- 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 :
  ∀ (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

Tactic:
rw [linearIndependent_iff_finset_linearIndependent] at h ⊢

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
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)
⊢ FiniteDimensional.{u, v} F ↥E'

Tactic:
haveI : FiniteDimensional F E' := finiteDimensional_adjoin
    fun x _ ↦ Algebra.IsIntegral.isIntegral x
-- 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 : ι)) ⋯
⊢ LinearIndependent F v'

Tactic:
have h' : LinearIndependent F v' := (h s).of_comp E'.val.toLinearMap