-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem Field.span_map_pow_expChar_pow_eq_top_of_isSeparable [Algebra.IsSeparable F E]
    (h : Submodule.span F (Set.range v) = ⊤) :
    Submodule.span F (Set.range (v · ^ q ^ n)) = ⊤

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
⊢ Submodule.span F (Set.range fun x => v x ^ q ^ n) = Submodule.span F ↑(MonoidHom.mrange (powMonoidHom (q ^ n)))

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

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
⊢ Set.range (DivisionSemiring.toSemiring.8 (q ^ n)) ⊆
    ↑(Submodule.span F (Set.range (DivisionSemiring.toSemiring.8 (q ^ n) ∘ v)))

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
⊢ Set.range (DivisionSemiring.toSemiring.8 (q ^ n)) ⊆
    ↑(Submodule.span F (Set.range (DivisionSemiring.toSemiring.8 (q ^ n) ∘ v)))

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

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
⊢ DivisionSemiring.toSemiring.8 (q ^ n) '' Set.univ ⊆
    ↑(Submodule.span F (DivisionSemiring.toSemiring.8 (q ^ n) '' Set.range v))

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
this : ExpChar E q
⊢ DivisionSemiring.toSemiring.8 (q ^ n) '' Set.univ ⊆
    ↑(Submodule.span F (DivisionSemiring.toSemiring.8 (q ^ n) '' Set.range v))

Tactic:
apply h ▸ Submodule.image_span_subset_span (LinearMap.iterateFrobenius F E q n) _

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
⊢ Submodule.span F (Set.range fun x => v x ^ q ^ n) = ⊤

Tactic:
erw [← Algebra.top_toSubmodule, ← top_toSubalgebra, ← adjoin_univ,
  adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable' F E _ q n,
  adjoin_algebraic_toSubalgebra fun x _ ↦ Algebra.IsAlgebraic.isAlgebraic x,
  Set.image_univ, Algebra.adjoin_eq_span, (powMonoidHom _).mrange.closure_eq]

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
⊢ Submodule.span F (Set.range fun x => v x ^ q ^ n) = Submodule.span F ↑(MonoidHom.mrange (powMonoidHom (q ^ n)))

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
⊢ DivisionSemiring.toSemiring.8 (q ^ n) '' Set.univ ⊆
    ↑(Submodule.span F (DivisionSemiring.toSemiring.8 (q ^ n) '' Set.range v))

Tactic:
haveI := expChar_of_injective_algebraMap (algebraMap F E).injective q

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
this : ExpChar E q
⊢ DivisionSemiring.toSemiring.8 (q ^ n) '' Set.univ ⊆
    ↑(Submodule.span F (DivisionSemiring.toSemiring.8 (q ^ n) '' Set.range v))