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
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}ᶜ
⊢ ∃ (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:
refine ⟨i, hi.comp_equiv e₂.symm, by convert! 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
n : ι
inst_3 : ExpChar k p
ha : Eq (α := IntermediateField k K) (adjoin k (Set.range a)) ⊤
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
have :
  ∀ (i : ι)
    (hi :
      (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
        IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)),
    ∃ (i : ι),
      (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
        Algebra.IsSeparable (↥(adjoin k (a '' {i}ᶜ))) K
⊢ ∃ (i : ι),
    (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
      Algebra.IsSeparable (↥(adjoin k (a '' {i}ᶜ))) K

Tactic:
have ⟨i, hi⟩ := exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow p hp H n ha'
-- 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 : Eq (α := IntermediateField k K) (adjoin k (Set.range a)) ⊤
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
i : ι
hi :
  (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
    IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
⊢ ∃ (i : ι),
    (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
      Algebra.IsSeparable (↥(adjoin k (a '' {i}ᶜ))) K

Tactic:
⟨i, hi.1, ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- 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 : Eq (α := IntermediateField k K) (adjoin k (Set.range a)) ⊤
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
i : ι
hi :
  (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
    IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
refine : Algebra.IsSeparable (↥(adjoin k (a '' {i}ᶜ))) K
⊢ ∃ (i : ι),
    (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
      Algebra.IsSeparable (↥(adjoin k (a '' {i}ᶜ))) K

Tactic:
refine ⟨i, hi.1, ?_⟩
-- 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 : Eq (α := IntermediateField k K) (adjoin k (Set.range a)) ⊤
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
i : ι
hi :
  (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
    IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
rw :
  Set.range a ⊆
    (↑(restrictScalars k (L' := ↥(adjoin k (a '' {i}ᶜ))) (separableClosure (↥(adjoin k (a '' {i}ᶜ))) K)) : Set K)
⊢ Algebra.IsSeparable (↥(adjoin k (a '' {i}ᶜ))) K

Tactic:
rw [← separableClosure.eq_top_iff, ← (restrictScalars_injective k).eq_iff,
    restrictScalars_top, eq_top_iff, ← ha, adjoin_le_iff]

Premises used: eq_top_iff, IntermediateField.adjoin_le_iff, IntermediateField.restrictScalars_top, Function.Injective.eq_iff, separableClosure.eq_top_iff, IntermediateField.restrictScalars_injective
-- 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 : Eq (α := IntermediateField k K) (adjoin k (Set.range a)) ⊤
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
i : ι
hi :
  (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
    IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
x : ι
inl :
  ∀
    (hi :
      (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ x }) ↦ a (↑j : ι)) ∧
        IsSeparable (↥(adjoin k (a '' {x}ᶜ))) (a x)),
    a x ∈ (↑(restrictScalars k (L' := ↥(adjoin k (a '' {x}ᶜ))) (separableClosure (↥(adjoin k (a '' {x}ᶜ))) K)) : Set K)
inr :
  ∀ (ne : x ≠ i),
    a x ∈ (↑(restrictScalars k (L' := ↥(adjoin k (a '' {i}ᶜ))) (separableClosure (↥(adjoin k (a '' {i}ᶜ))) K)) : Set K)
⊢ a x ∈ (↑(restrictScalars k (L' := ↥(adjoin k (a '' {i}ᶜ))) (separableClosure (↥(adjoin k (a '' {i}ᶜ))) K)) : Set K)

Tactic:
obtain rfl | ne := eq_or_ne x i

Premises used: eq_or_ne, rfl
-- 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 : Eq (α := IntermediateField k K) (adjoin k (Set.range a)) ⊤
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
x : ι
hi :
  (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ x }) ↦ a (↑j : ι)) ∧
    IsSeparable (↥(adjoin k (a '' {x}ᶜ))) (a x)
⊢ a x ∈ (↑(restrictScalars k (L' := ↥(adjoin k (a '' {x}ᶜ))) (separableClosure (↥(adjoin k (a '' {x}ᶜ))) K)) : Set K)

Tactic:
hi.2

Premises used: Set.Mem, setOf, And.right, IsSeparable, Polynomial.Separable, IsCoprime
-- 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 : Eq (α := IntermediateField k K) (adjoin k (Set.range a)) ⊤
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
x : ι
hi :
  (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ x }) ↦ a (↑j : ι)) ∧
    IsSeparable (↥(adjoin k (a '' {x}ᶜ))) (a x)
⊢ a x ∈ (↑(restrictScalars k (L' := ↥(adjoin k (a '' {x}ᶜ))) (separableClosure (↥(adjoin k (a '' {x}ᶜ))) K)) : Set K)

Tactic:
exact hi.2

Premises used: And.right
-- 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 : Eq (α := IntermediateField k K) (adjoin k (Set.range a)) ⊤
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
i : ι
hi :
  (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
    IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
x : ι
ne : x ≠ i
⊢ a x ∈ (↑(restrictScalars k (L' := ↥(adjoin k (a '' {i}ᶜ))) (separableClosure (↥(adjoin k (a '' {i}ᶜ))) K)) : Set K)

Tactic:
isSeparable_algebraMap (F := adjoin k (a '' {i}ᶜ)) ⟨_, subset_adjoin _ _ ⟨x, ne, rfl⟩⟩

Premises used: Set.Mem, isSeparable_algebraMap, setOf, IntermediateField.subset_adjoin, Subtype.mk, And.intro, Exists.intro, IsSeparable, Polynomial.Separable, rfl, IsCoprime
-- 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 : Eq (α := IntermediateField k K) (adjoin k (Set.range a)) ⊤
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
i : ι
hi :
  (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
    IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
x : ι
ne : x ≠ i
⊢ a x ∈ (↑(restrictScalars k (L' := ↥(adjoin k (a '' {i}ᶜ))) (separableClosure (↥(adjoin k (a '' {i}ᶜ))) K)) : Set K)

Tactic:
exact isSeparable_algebraMap (F := adjoin k (a '' {i}ᶜ)) ⟨_, subset_adjoin _ _ ⟨x, ne, rfl⟩⟩

Premises used: isSeparable_algebraMap, IntermediateField.subset_adjoin, Subtype.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
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)
inst_3 : ExpChar k p
inst_4 : Algebra.EssFiniteType k K
have :
  ∀ (s : Finset K)
    (hs :
      IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ (↑s : Set K) }) k
        (Subtype.val (p := fun (x : K) ↦ x ∈ (↑s : Set K))))
    (Hs :
      ∀ ⦃j : Set K⦄,
        (fun (t : Set K) ↦
              IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t)))
            j →
          LE.le.{u_2} (α := IntermediateField k K)
              ((fun (t : Set K) ↦
                  (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) :
                    IntermediateField k K))
                (↑s : Set K))
              ((fun (t : Set K) ↦
                  (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) :
                    IntermediateField k K))
                j) →
            LE.le.{u_2} (α := IntermediateField k K)
              ((fun (t : Set K) ↦
                  (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) :
                    IntermediateField k K))
                j)
              ((fun (t : Set K) ↦
                  (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) :
                    IntermediateField k K))
                (↑s : Set K))),
    ∃ (s : Finset K),
      IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
        Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K
⊢ ∃ (s : Finset K),
    IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
      Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K

Tactic:
have ⟨s, hs, Hs⟩ := exists_finset_maximalFor_isTranscendenceBasis_separableClosure k K
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
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)
inst_3 : ExpChar k p
inst_4 : Algebra.EssFiniteType k K
s : Finset K
hs :
  (fun (t : Set K) ↦
      IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t)))
    (↑s : Set K)
Hs :
  ∀ ⦃j : Set K⦄,
    (fun (t : Set K) ↦
          IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t)))
        j →
      LE.le.{u_2} (α := IntermediateField k K)
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            (↑s : Set K))
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            j) →
        LE.le.{u_2} (α := IntermediateField k K)
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            j)
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            (↑s : Set K))
⊢ ∃ (s : Finset K),
    IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
      Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K

Tactic:
⟨s, hs, ⟨fun n ↦ of_not_not fun hn ↦ ?_⟩⟩

Premises used: And.intro, Exists.intro, of_not_not, Algebra.IsSeparable.mk
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
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)
inst_3 : ExpChar k p
inst_4 : Algebra.EssFiniteType k K
s : Finset K
hs :
  (fun (t : Set K) ↦
      IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t)))
    (↑s : Set K)
Hs :
  ∀ ⦃j : Set K⦄,
    (fun (t : Set K) ↦
          IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t)))
        j →
      LE.le.{u_2} (α := IntermediateField k K)
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            (↑s : Set K))
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            j) →
        LE.le.{u_2} (α := IntermediateField k K)
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            j)
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            (↑s : Set K))
refine : ∀ (n : K) (hn : ¬IsSeparable (↥(adjoin k (↑s : Set K))) n), False
⊢ ∃ (s : Finset K),
    IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) k (Subtype.val (p := fun (x : K) ↦ x ∈ s)) ∧
      Algebra.IsSeparable (↥(adjoin k (↑s : Set K))) K

Tactic:
refine ⟨s, hs, ⟨fun n ↦ of_not_not fun hn ↦ ?_⟩⟩
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
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)
inst_3 : ExpChar k p
inst_4 : Algebra.EssFiniteType k K
s : Finset K
hs :
  (fun (t : Set K) ↦
      IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t)))
    (↑s : Set K)
Hs :
  ∀ ⦃j : Set K⦄,
    (fun (t : Set K) ↦
          IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t)))
        j →
      LE.le.{u_2} (α := IntermediateField k K)
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            (↑s : Set K))
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            j) →
        LE.le.{u_2} (α := IntermediateField k K)
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            j)
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            (↑s : Set K))
n : K
hn : ¬IsSeparable (↥(adjoin k (↑s : Set K))) n
⊢ n ∉ s

Tactic:
have hns : n ∉ s := fun h ↦ hn (le_restrictScalars_separableClosure _ (subset_adjoin _ _ h))
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
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)
inst_3 : ExpChar k p
inst_4 : Algebra.EssFiniteType k K
s : Finset K
hs :
  (fun (t : Set K) ↦
      IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t)))
    (↑s : Set K)
Hs :
  ∀ ⦃j : Set K⦄,
    (fun (t : Set K) ↦
          IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t)))
        j →
      LE.le.{u_2} (α := IntermediateField k K)
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            (↑s : Set K))
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            j) →
        LE.le.{u_2} (α := IntermediateField k K)
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            j)
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            (↑s : Set K))
n : K
hn : ¬IsSeparable (↥(adjoin k (↑s : Set K))) n
hns : n ∉ s
have :
  ∀ (i : K) (hi₁ : IsTranscendenceBasis k (A := K) fun (j : (↑(insert n (↑s : Set K) \ {i}) : Type u_2)) ↦ id (↑j : K))
    (hi₂ : IsSeparable (↥(adjoin k (id '' (insert n (↑s : Set K) \ {i})))) (id i)), False
⊢ False

Tactic:
have ⟨i, hi₁, hi₂⟩ := exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow'
    p hp (a := id) H s n hs hns
-- Module: Mathlib.FieldTheory.SeparablyGenerated
Goal:
k : Type u_1
K : Type u_2
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)
inst_3 : ExpChar k p
inst_4 : Algebra.EssFiniteType k K
s : Finset K
hs :
  (fun (t : Set K) ↦
      IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t)))
    (↑s : Set K)
Hs :
  ∀ ⦃j : Set K⦄,
    (fun (t : Set K) ↦
          IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t)))
        j →
      LE.le.{u_2} (α := IntermediateField k K)
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            (↑s : Set K))
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            j) →
        LE.le.{u_2} (α := IntermediateField k K)
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            j)
          ((fun (t : Set K) ↦
              (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
            (↑s : Set K))
n : K
hn : ¬IsSeparable (↥(adjoin k (↑s : Set K))) n
hns : n ∉ s
i : K
hi₁ : IsTranscendenceBasis k (A := K) fun (j : (↑(insert n (↑s : Set K) \ {i}) : Type u_2)) ↦ id (↑j : K)
hi₂ : IsSeparable (↥(adjoin k (id '' (insert n (↑s : Set K) \ {i})))) (id i)
⊢ IsSeparable (↥(adjoin k (insert n (↑s : Set K) \ {i}))) (id i)

Tactic:
rw [Set.image_id] at hi₂

Premises used: Set.image_id