-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem LinearIndependent.map_pow_expChar_pow_of_isSeparable [Algebra.IsSeparable F E]
    (h : LinearIndependent F v) : LinearIndependent F (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 : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
halg : Algebra.IsAlgebraic F E
s : Finset ι
E' : IntermediateField F E := adjoin F ↑(Finset.image v s)
⊢ LinearIndependent F ((fun x => v x ^ q ^ n) ∘ Subtype.val)

Tactic:
haveI : FiniteDimensional F E' := finiteDimensional_adjoin
  fun x _ ↦ Algebra.IsIntegral.isIntegral x

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 : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
halg : Algebra.IsAlgebraic F E
s : Finset ι
E' : IntermediateField F E := adjoin F ↑(Finset.image v s)
this : FiniteDimensional F ↥E'
⊢ LinearIndependent F ((fun x => v x ^ q ^ n) ∘ Subtype.val)

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 : LinearIndependent F v
⊢ LinearIndependent F fun x => v x ^ q ^ n

Tactic:
have halg := Algebra.IsSeparable.isAlgebraic F E

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 : LinearIndependent F v
halg : Algebra.IsAlgebraic F E
⊢ LinearIndependent F fun x => v x ^ 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 : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
halg : Algebra.IsAlgebraic F E
s : Finset ι
E' : IntermediateField F E := adjoin F ↑(Finset.image v s)
this : FiniteDimensional F ↥E'
⊢ LinearIndependent F ((fun x => v x ^ q ^ n) ∘ Subtype.val)

Tactic:
haveI : Algebra.IsSeparable F E' := Algebra.isSeparable_tower_bot_of_isSeparable F E' E

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 : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
halg : Algebra.IsAlgebraic F E
s : Finset ι
E' : IntermediateField F E := adjoin F ↑(Finset.image v s)
this✝ : FiniteDimensional F ↥E'
this : Algebra.IsSeparable F ↥E'
⊢ LinearIndependent F ((fun x => v x ^ q ^ n) ∘ Subtype.val)

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 : LinearIndependent F v
halg : Algebra.IsAlgebraic F E
⊢ LinearIndependent F fun x => v x ^ q ^ n

Tactic:
rw [linearIndependent_iff_finset_linearIndependent] at h ⊢

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 : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
halg : Algebra.IsAlgebraic F E
⊢ ∀ (s : Finset ι), LinearIndependent F ((fun x => v x ^ q ^ n) ∘ Subtype.val)

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 : LinearIndependent F v
⊢ LinearIndependent F fun x => v x ^ q ^ n

Tactic:
classical
have halg := Algebra.IsSeparable.isAlgebraic F E
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
haveI : Algebra.IsSeparable F E' := Algebra.isSeparable_tower_bot_of_isSeparable F E' E
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)

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 : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
halg : Algebra.IsAlgebraic F E
⊢ ∀ (s : Finset ι), LinearIndependent F ((fun x => v x ^ q ^ n) ∘ Subtype.val)

Tactic:
intro s

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 : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
halg : Algebra.IsAlgebraic F E
s : Finset ι
⊢ LinearIndependent F ((fun x => v x ^ q ^ n) ∘ Subtype.val)

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 : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
halg : Algebra.IsAlgebraic F E
s : Finset ι
E' : IntermediateField F E := adjoin F ↑(Finset.image v s)
this✝ : FiniteDimensional F ↥E'
this : Algebra.IsSeparable F ↥E'
v' : { x // x ∈ s } → ↥E' := fun i => ⟨v ↑i, ⋯⟩
h' : LinearIndependent F v'
⊢ LinearIndependent F ((fun x => v x ^ q ^ n) ∘ Subtype.val)

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)

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 : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
halg : Algebra.IsAlgebraic F E
s : Finset ι
E' : IntermediateField F E := adjoin F ↑(Finset.image v s)
this✝ : FiniteDimensional F ↥E'
this : Algebra.IsSeparable F ↥E'
⊢ LinearIndependent F ((fun x => v x ^ q ^ n) ∘ Subtype.val)

Tactic:
let v' (i : s) : E' := ⟨v i.1, subset_adjoin F _ (Finset.mem_image.2 ⟨i.1, i.2, rfl⟩)⟩

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 : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
halg : Algebra.IsAlgebraic F E
s : Finset ι
E' : IntermediateField F E := adjoin F ↑(Finset.image v s)
this✝ : FiniteDimensional F ↥E'
this : Algebra.IsSeparable F ↥E'
v' : { x // x ∈ s } → ↥E' := fun i => ⟨v ↑i, ⋯⟩
⊢ LinearIndependent F ((fun x => v x ^ q ^ n) ∘ Subtype.val)

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 : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
halg : Algebra.IsAlgebraic F E
s : Finset ι
E' : IntermediateField F E := adjoin F ↑(Finset.image v s)
this✝ : FiniteDimensional F ↥E'
this : Algebra.IsSeparable F ↥E'
v' : { x // x ∈ s } → ↥E' := fun i => ⟨v ↑i, ⋯⟩
⊢ LinearIndependent F ((fun x => v x ^ q ^ n) ∘ Subtype.val)

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

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 : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
halg : Algebra.IsAlgebraic F E
s : Finset ι
E' : IntermediateField F E := adjoin F ↑(Finset.image v s)
this✝ : FiniteDimensional F ↥E'
this : Algebra.IsSeparable F ↥E'
v' : { x // x ∈ s } → ↥E' := fun i => ⟨v ↑i, ⋯⟩
h' : LinearIndependent F v'
⊢ LinearIndependent F ((fun x => v x ^ q ^ n) ∘ Subtype.val)