awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
F : MvPolynomial ι k
hFmin :
  ∀ (G : MvPolynomial ι k),
    G ≠ 0 → Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) G : K) (0 : K) → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ (σ : (a : ι) → ℕ) i
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (x : { x : ι // x ≠ i }) ↦ a (↑x : ι)
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (M := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (F.toPolynomialAdjoinImageCompl a i)
this_1 : UniqueFactorizationMonoid.{u_2} ↥(Algebra.adjoin k (a '' {i}ᶜ))
hF₂irr :
  Irreducible (M := Polynomial ↥k')
    (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
      (F.toPolynomialAdjoinImageCompl a i))
Hsep : ¬IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
this : CharP.{u_2} (↥k') p
obtain :
  ∀ (g : Polynomial ↥k') (hg : Irreducible g)
    (eq :
      Eq (α := Polynomial ↥k') ((Polynomial.expand (↥k') p : (a : Polynomial ↥k') → Polynomial ↥k') g : Polynomial ↥k')
        (minpoly (↥k') (a i) : Polynomial ↥k')),
    Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
      (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
⊢ Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0

Tactic:
obtain ⟨g, hg, eq⟩ := (((minpoly k' (a i)).separable_or p (minpoly.irreducible
    (isAlgebraic_iff_isIntegral.mp <| isAlgebraic_adjoin_iff.mpr alg))).resolve_left Hsep).2

Premises used: Iff.mpr, IntermediateField.isAlgebraic_adjoin_iff, Polynomial.separable_or, Or.resolve_left, And.right, Iff.mp, minpoly.irreducible, isAlgebraic_iff_isIntegral
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
F : MvPolynomial ι k
hFmin :
  ∀ (G : MvPolynomial ι k),
    G ≠ 0 → Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) G : K) (0 : K) → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ (σ : (a : ι) → ℕ) i
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (x : { x : ι // x ≠ i }) ↦ a (↑x : ι)
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (M := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (F.toPolynomialAdjoinImageCompl a i)
this_1 : UniqueFactorizationMonoid.{u_2} ↥(Algebra.adjoin k (a '' {i}ᶜ))
hF₂irr :
  Irreducible (M := Polynomial ↥k')
    (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
      (F.toPolynomialAdjoinImageCompl a i))
Hsep : ¬IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
this : CharP.{u_2} (↥k') p
g : Polynomial ↥k'
hg : Irreducible g
eq :
  Eq (α := Polynomial ↥k') ((Polynomial.expand (↥k') p : (a : Polynomial ↥k') → Polynomial ↥k') g : Polynomial ↥k')
    (minpoly (↥k') (a i) : Polynomial ↥k')
⊢ Eq (α := ↥k')
    (Polynomial.coeff ((Polynomial.expand (↥k') p : (a : Polynomial ↥k') → Polynomial ↥k') g) ((σ : (a : ι) → ℕ) i))
    (Polynomial.coeff (minpoly (↥k') (a i)) ((σ : (a : ι) → ℕ) i))

Tactic:
replace eq := congr(Polynomial.coeff $eq (σ i))
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
F : MvPolynomial ι k
hFmin :
  ∀ (G : MvPolynomial ι k),
    G ≠ 0 → Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) G : K) (0 : K) → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ (σ : (a : ι) → ℕ) i
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (x : { x : ι // x ≠ i }) ↦ a (↑x : ι)
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (M := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (F.toPolynomialAdjoinImageCompl a i)
this_1 : UniqueFactorizationMonoid.{u_2} ↥(Algebra.adjoin k (a '' {i}ᶜ))
hF₂irr :
  Irreducible (M := Polynomial ↥k')
    (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
      (F.toPolynomialAdjoinImageCompl a i))
Hsep : ¬IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
this : CharP.{u_2} (↥k') p
g : Polynomial ↥k'
hg : Irreducible g
eq :
  0 =
    HMul.hMul (α := ↥k')
      (Polynomial.coeff
        (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
          (F.toPolynomialAdjoinImageCompl a i))
        ((σ : (a : ι) → ℕ) i))
      (Polynomial.leadingCoeff
          (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
            (F.toPolynomialAdjoinImageCompl a i)))⁻¹
⊢ Ne (α := ↥k')
    (Polynomial.leadingCoeff
      (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
        (F.toPolynomialAdjoinImageCompl a i)))
    0

Tactic:
simpa using hF₂irr.ne_zero

Premises used: Irreducible.ne_zero
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
inst_3 : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : (↑s : Type u_3)) ↦ a (↑i : ι)
hn : n ∉ s
j : (↑(insert n s) : Type u_3)
⊢ n ∈ insert n s

Tactic:
simp
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
inst_3 : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : (↑s : Type u_3)) ↦ a (↑i : ι)
hn : n ∉ s
x : { j : (↑(insert n s) : Type u_3) // j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯ }
⊢ (↑(↑x : (↑(insert n s) : Type u_3)) : ι) ∈ s

Tactic:
aesop
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
inst_3 : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : (↑s : Type u_3)) ↦ a (↑i : ι)
hn : n ∉ s
x : (↑s : Type u_3)
⊢ (↑x : ι) ∈ insert n s

Tactic:
aesop
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
inst_3 : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : (↑s : Type u_3)) ↦ a (↑i : ι)
hn : n ∉ s
x : (↑s : Type u_3)
⊢ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) (↑x : ι) ⋯ ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯

Tactic:
aesop
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
inst_3 : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : (↑s : Type u_3)) ↦ a (↑i : ι)
hn : n ∉ s
e₁ : { j : (↑(insert n s) : Type u_3) // j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯ } ≃ (↑s : Type u_3) :=
  {
    toFun := fun (x : { j : (↑(insert n s) : Type u_3) // j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯ }) ↦
      Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑(↑x : (↑(insert n s) : Type u_3)) : ι) ⋯,
    invFun := fun (x : (↑s : Type u_3)) ↦
      Subtype.mk (p := fun (j : (↑(insert n s) : Type u_3)) ↦ j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) (↑x : ι) ⋯) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
⊢ n ∈ insert n s

Tactic:
simp
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
inst_3 : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : (↑s : Type u_3)) ↦ a (↑i : ι)
hn : n ∉ s
e₁ : { j : (↑(insert n s) : Type u_3) // j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯ } ≃ (↑s : Type u_3) :=
  {
    toFun := fun (x : { j : (↑(insert n s) : Type u_3) // j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯ }) ↦
      Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑(↑x : (↑(insert n s) : Type u_3)) : ι) ⋯,
    invFun := fun (x : (↑s : Type u_3)) ↦
      Subtype.mk (p := fun (j : (↑(insert n s) : Type u_3)) ↦ j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) (↑x : ι) ⋯) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
obtain :
  ∀ (i : (↑(insert n s) : Type u_3))
    (hi :
      IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : (↑(insert n s) : Type u_3) // j ≠ i }) ↦
        a (↑(↑j : (↑(insert n s) : Type u_3)) : ι))
    (hi' : IsSeparable (↥(adjoin k ((fun (i : (↑(insert n s) : Type u_3)) ↦ a (↑i : ι)) '' {i}ᶜ))) (a (↑i : ι))),
    ∃ (i : ι),
      (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : (↑(insert n s \ {i}) : Type u_3)) ↦ a (↑j : ι)) ∧
        IsSeparable (↥(adjoin k (a '' (insert n s \ {i})))) (a i)
⊢ ∃ (i : ι),
    (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : (↑(insert n s \ {i}) : Type u_3)) ↦ a (↑j : ι)) ∧
      IsSeparable (↥(adjoin k (a '' (insert n s \ {i})))) (a i)

Tactic:
obtain ⟨i, hi, hi'⟩ := exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow p hp H
    (a := fun i : ↥(insert n s) ↦ a i) ⟨n, by simp⟩ (ha.comp_equiv e₁)

Premises used: Subtype.mk, IsTranscendenceBasis.comp_equiv, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
inst_3 : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : (↑s : Type u_3)) ↦ a (↑i : ι)
hn : n ∉ s
e₁ : { j : (↑(insert n s) : Type u_3) // j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯ } ≃ (↑s : Type u_3) :=
  {
    toFun := fun (x : { j : (↑(insert n s) : Type u_3) // j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯ }) ↦
      Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑(↑x : (↑(insert n s) : Type u_3)) : ι) ⋯,
    invFun := fun (x : (↑s : Type u_3)) ↦
      Subtype.mk (p := fun (j : (↑(insert n s) : Type u_3)) ↦ j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) (↑x : ι) ⋯) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
i : (↑(insert n s) : Type u_3)
hi :
  IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : (↑(insert n s) : Type u_3) // j ≠ i }) ↦
    a (↑(↑j : (↑(insert n s) : Type u_3)) : ι)
hi' : IsSeparable (↥(adjoin k ((fun (i : (↑(insert n s) : Type u_3)) ↦ a (↑i : ι)) '' {i}ᶜ))) (a (↑i : ι))
e₂ : { j : (↑(insert n s) : Type u_3) // j ≠ i } ≃ (↑(insert n s \ {(↑i : ι)}) : Type u_3) :=
  {
    toFun := fun (x : { j : (↑(insert n s) : Type u_3) // j ≠ i }) ↦
      Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s \ {(↑i : ι)}) (↑(↑x : (↑(insert n s) : Type u_3)) : ι) ⋯,
    invFun := fun (x : (↑(insert n s \ {(↑i : ι)}) : Type u_3)) ↦
      Subtype.mk (p := fun (j : (↑(insert n s) : Type u_3)) ↦ j ≠ i)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) (↑x : ι) ⋯) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
h :
  ∀ (x : K),
    x ∈ a '' (insert n s \ {(↑i : ι)}) ↔
      Membership.mem (γ := Set K) ((fun (x : (↑(insert n s) : Type u_3)) ↦ a (↑x : ι)) '' {i}ᶜ) x
⊢ a '' (insert n s \ {(↑i : ι)}) = (fun (x : (↑(insert n s) : Type u_3)) ↦ a (↑x : ι)) '' {i}ᶜ

Tactic:
ext
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
inst_3 : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : (↑s : Type u_3)) ↦ a (↑i : ι)
hn : n ∉ s
e₁ : { j : (↑(insert n s) : Type u_3) // j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯ } ≃ (↑s : Type u_3) :=
  {
    toFun := fun (x : { j : (↑(insert n s) : Type u_3) // j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯ }) ↦
      Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑(↑x : (↑(insert n s) : Type u_3)) : ι) ⋯,
    invFun := fun (x : (↑s : Type u_3)) ↦
      Subtype.mk (p := fun (j : (↑(insert n s) : Type u_3)) ↦ j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) (↑x : ι) ⋯) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
i : (↑(insert n s) : Type u_3)
hi :
  IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : (↑(insert n s) : Type u_3) // j ≠ i }) ↦
    a (↑(↑j : (↑(insert n s) : Type u_3)) : ι)
hi' : IsSeparable (↥(adjoin k ((fun (i : (↑(insert n s) : Type u_3)) ↦ a (↑i : ι)) '' {i}ᶜ))) (a (↑i : ι))
e₂ : { j : (↑(insert n s) : Type u_3) // j ≠ i } ≃ (↑(insert n s \ {(↑i : ι)}) : Type u_3) :=
  {
    toFun := fun (x : { j : (↑(insert n s) : Type u_3) // j ≠ i }) ↦
      Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s \ {(↑i : ι)}) (↑(↑x : (↑(insert n s) : Type u_3)) : ι) ⋯,
    invFun := fun (x : (↑(insert n s \ {(↑i : ι)}) : Type u_3)) ↦
      Subtype.mk (p := fun (j : (↑(insert n s) : Type u_3)) ↦ j ≠ i)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) (↑x : ι) ⋯) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
x : K
⊢ x ∈ a '' (insert n s \ {(↑i : ι)}) ↔
    Membership.mem (γ := Set K) ((fun (x : (↑(insert n s) : Type u_3)) ↦ a (↑x : ι)) '' {i}ᶜ) x

Tactic:
aesop
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
inst_3 : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : (↑s : Type u_3)) ↦ a (↑i : ι)
hn : n ∉ s
e₁ : { j : (↑(insert n s) : Type u_3) // j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯ } ≃ (↑s : Type u_3) :=
  {
    toFun := fun (x : { j : (↑(insert n s) : Type u_3) // j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯ }) ↦
      Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑(↑x : (↑(insert n s) : Type u_3)) : ι) ⋯,
    invFun := fun (x : (↑s : Type u_3)) ↦
      Subtype.mk (p := fun (j : (↑(insert n s) : Type u_3)) ↦ j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) (↑x : ι) ⋯) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
i : (↑(insert n s) : Type u_3)
hi :
  IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : (↑(insert n s) : Type u_3) // j ≠ i }) ↦
    a (↑(↑j : (↑(insert n s) : Type u_3)) : ι)
hi' : IsSeparable (↥(adjoin k ((fun (i : (↑(insert n s) : Type u_3)) ↦ a (↑i : ι)) '' {i}ᶜ))) (a (↑i : ι))
e₂ : { j : (↑(insert n s) : Type u_3) // j ≠ i } ≃ (↑(insert n s \ {(↑i : ι)}) : Type u_3) :=
  {
    toFun := fun (x : { j : (↑(insert n s) : Type u_3) // j ≠ i }) ↦
      Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s \ {(↑i : ι)}) (↑(↑x : (↑(insert n s) : Type u_3)) : ι) ⋯,
    invFun := fun (x : (↑(insert n s \ {(↑i : ι)}) : Type u_3)) ↦
      Subtype.mk (p := fun (j : (↑(insert n s) : Type u_3)) ↦ j ≠ i)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) (↑x : ι) ⋯) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
⊢ a '' (insert n s \ {(↑i : ι)}) = (fun (x : (↑(insert n s) : Type u_3)) ↦ a (↑x : ι)) '' {i}ᶜ

Tactic:
have : a '' (insert n s \ {i.1}) = (a ·.1) '' {i}ᶜ := by ext; aesop
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
inst_3 : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : (↑s : Type u_3)) ↦ a (↑i : ι)
hn : n ∉ s
e₁ : { j : (↑(insert n s) : Type u_3) // j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯ } ≃ (↑s : Type u_3) :=
  {
    toFun := fun (x : { j : (↑(insert n s) : Type u_3) // j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯ }) ↦
      Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑(↑x : (↑(insert n s) : Type u_3)) : ι) ⋯,
    invFun := fun (x : (↑s : Type u_3)) ↦
      Subtype.mk (p := fun (j : (↑(insert n s) : Type u_3)) ↦ j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) (↑x : ι) ⋯) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
i : (↑(insert n s) : Type u_3)
hi :
  IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : (↑(insert n s) : Type u_3) // j ≠ i }) ↦
    a (↑(↑j : (↑(insert n s) : Type u_3)) : ι)
hi' : IsSeparable (↥(adjoin k ((fun (i : (↑(insert n s) : Type u_3)) ↦ a (↑i : ι)) '' {i}ᶜ))) (a (↑i : ι))
e₂ : { j : (↑(insert n s) : Type u_3) // j ≠ i } ≃ (↑(insert n s \ {(↑i : ι)}) : Type u_3) :=
  {
    toFun := fun (x : { j : (↑(insert n s) : Type u_3) // j ≠ i }) ↦
      Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s \ {(↑i : ι)}) (↑(↑x : (↑(insert n s) : Type u_3)) : ι) ⋯,
    invFun := fun (x : (↑(insert n s \ {(↑i : ι)}) : Type u_3)) ↦
      Subtype.mk (p := fun (j : (↑(insert n s) : Type u_3)) ↦ j ≠ i)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) (↑x : ι) ⋯) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
this : a '' (insert n s \ {(↑i : ι)}) = (fun (x : (↑(insert n s) : Type u_3)) ↦ a (↑x : ι)) '' {i}ᶜ
⊢ IsSeparable (↥(adjoin k ((fun (i : (↑(insert n s) : Type u_3)) ↦ a (↑i : ι)) '' {i}ᶜ))) (a (↑i : ι))

Tactic:
hi'
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
inst_3 : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : (↑s : Type u_3)) ↦ a (↑i : ι)
hn : n ∉ s
e₁ : { j : (↑(insert n s) : Type u_3) // j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯ } ≃ (↑s : Type u_3) :=
  {
    toFun := fun (x : { j : (↑(insert n s) : Type u_3) // j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯ }) ↦
      Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑(↑x : (↑(insert n s) : Type u_3)) : ι) ⋯,
    invFun := fun (x : (↑s : Type u_3)) ↦
      Subtype.mk (p := fun (j : (↑(insert n s) : Type u_3)) ↦ j ≠ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) n ⋯)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) (↑x : ι) ⋯) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
i : (↑(insert n s) : Type u_3)
hi :
  IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : (↑(insert n s) : Type u_3) // j ≠ i }) ↦
    a (↑(↑j : (↑(insert n s) : Type u_3)) : ι)
hi' : IsSeparable (↥(adjoin k ((fun (i : (↑(insert n s) : Type u_3)) ↦ a (↑i : ι)) '' {i}ᶜ))) (a (↑i : ι))
e₂ : { j : (↑(insert n s) : Type u_3) // j ≠ i } ≃ (↑(insert n s \ {(↑i : ι)}) : Type u_3) :=
  {
    toFun := fun (x : { j : (↑(insert n s) : Type u_3) // j ≠ i }) ↦
      Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s \ {(↑i : ι)}) (↑(↑x : (↑(insert n s) : Type u_3)) : ι) ⋯,
    invFun := fun (x : (↑(insert n s \ {(↑i : ι)}) : Type u_3)) ↦
      Subtype.mk (p := fun (j : (↑(insert n s) : Type u_3)) ↦ j ≠ i)
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert n s) (↑x : ι) ⋯) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
this : a '' (insert n s \ {(↑i : ι)}) = (fun (x : (↑(insert n s) : Type u_3)) ↦ a (↑x : ι)) '' {i}ᶜ
⊢ IsSeparable (↥(adjoin k (a '' (insert n s \ {(↑i : ι)})))) (a (↑i : ι))

Tactic:
convert! hi'