awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (insert n (↑s : Set K) \ {i}))) (id i)
refine_1 :
  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))
      (insert n (↑s : Set K) \ {i}))
refine_2 :
  Membership.mem (γ := IntermediateField k K)
    ((fun (t : Set K) ↦
        (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
      (insert n (↑s : Set K) \ {i}))
    n
⊢ False

Tactic:
refine not_lt_iff_le_imp_ge.mpr (Hs hi₁) (SetLike.lt_iff_le_and_exists.mpr ⟨?_, n, ?_, hn⟩)

Premises used: Iff.mpr, SetLike.lt_iff_le_and_exists, And.intro, Exists.intro, not_lt_iff_le_imp_ge
-- 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 (insert n (↑s : Set K) \ {i}))) (id i)
refine_1 :
  (↑s : Set K) ⊆
    (↑(restrictScalars k (L' := ↥(adjoin k (insert n (↑s : Set K) \ {i})))
          (separableClosure (↥(adjoin k (insert n (↑s : Set K) \ {i}))) K)) :
      Set K)
⊢ 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))
      (insert n (↑s : Set K) \ {i}))

Tactic:
rw [separableClosure_le_separableClosure_iff, adjoin_le_iff]

Premises used: IntermediateField.adjoin_le_iff, separableClosure_le_separableClosure_iff
-- 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 (insert n (↑s : Set K) \ {i}))) (id i)
x : K
hx : x ∈ (↑s : Set K)
refine_1 :
  ∀ (hi₁ : IsTranscendenceBasis k (A := K) fun (j : (↑(insert n (↑s : Set K) \ {x}) : Type u_2)) ↦ id (↑j : K))
    (hi₂ : IsSeparable (↥(adjoin k (insert n (↑s : Set K) \ {x}))) (id x)),
    x ∈
      (↑(restrictScalars k (L' := ↥(adjoin k (insert n (↑s : Set K) \ {x})))
            (separableClosure (↥(adjoin k (insert n (↑s : Set K) \ {x}))) K)) :
        Set K)
refine_1₁ :
  ∀ (ne : x ≠ i),
    x ∈
      (↑(restrictScalars k (L' := ↥(adjoin k (insert n (↑s : Set K) \ {i})))
            (separableClosure (↥(adjoin k (insert n (↑s : Set K) \ {i}))) K)) :
        Set K)
⊢ x ∈
    (↑(restrictScalars k (L' := ↥(adjoin k (insert n (↑s : Set K) \ {i})))
          (separableClosure (↥(adjoin k (insert n (↑s : Set K) \ {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
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
x : K
hx : x ∈ (↑s : Set K)
hi₁ : IsTranscendenceBasis k (A := K) fun (j : (↑(insert n (↑s : Set K) \ {x}) : Type u_2)) ↦ id (↑j : K)
hi₂ : IsSeparable (↥(adjoin k (insert n (↑s : Set K) \ {x}))) (id x)
⊢ x ∈
    (↑(restrictScalars k (L' := ↥(adjoin k (insert n (↑s : Set K) \ {x})))
          (separableClosure (↥(adjoin k (insert n (↑s : Set K) \ {x}))) K)) :
      Set K)

Tactic:
hi₂

Premises used: Set.Mem, setOf, IsSeparable, Polynomial.Separable, IsCoprime
-- 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 (insert n (↑s : Set K) \ {i}))) (id i)
x : K
hx : x ∈ (↑s : Set K)
ne : x ≠ i
⊢ x ∈
    (↑(restrictScalars k (L' := ↥(adjoin k (insert n (↑s : Set K) \ {i})))
          (separableClosure (↥(adjoin k (insert n (↑s : Set K) \ {i}))) K)) :
      Set K)

Tactic:
le_restrictScalars_separableClosure _ (subset_adjoin _ _ ⟨.inr hx, ne⟩)

Premises used: IntermediateField.subset_adjoin, le_restrictScalars_separableClosure, And.intro, Or.inr
-- 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
x : K
hx : x ∈ (↑s : Set K)
hi₁ : IsTranscendenceBasis k (A := K) fun (j : (↑(insert n (↑s : Set K) \ {x}) : Type u_2)) ↦ id (↑j : K)
hi₂ : IsSeparable (↥(adjoin k (insert n (↑s : Set K) \ {x}))) (id x)
⊢ x ∈
    (↑(restrictScalars k (L' := ↥(adjoin k (insert n (↑s : Set K) \ {x})))
          (separableClosure (↥(adjoin k (insert n (↑s : Set K) \ {x}))) K)) :
      Set K)

Tactic:
exacts [hi₂, le_restrictScalars_separableClosure _ (subset_adjoin _ _ ⟨.inr hx, ne⟩)]
-- 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 (insert n (↑s : Set K) \ {i}))) (id i)
refine_2 :
  ∀ (hi₁ : IsTranscendenceBasis k (A := K) fun (j : (↑(insert n (↑s : Set K) \ {n}) : Type u_2)) ↦ id (↑j : K))
    (hi₂ : IsSeparable (↥(adjoin k (insert n (↑s : Set K) \ {n}))) (id n)),
    Membership.mem (γ := IntermediateField k K)
      ((fun (t : Set K) ↦
          (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
        (insert n (↑s : Set K) \ {n}))
      n
refine_2₁ :
  ∀ (ne : n ≠ i),
    Membership.mem (γ := IntermediateField k K)
      ((fun (t : Set K) ↦
          (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
        (insert n (↑s : Set K) \ {i}))
      n
⊢ Membership.mem (γ := IntermediateField k K)
    ((fun (t : Set K) ↦
        (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
      (insert n (↑s : Set K) \ {i}))
    n

Tactic:
obtain rfl | ne := eq_or_ne n i

Premises used: eq_or_ne, 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
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
hi₁ : IsTranscendenceBasis k (A := K) fun (j : (↑(insert n (↑s : Set K) \ {n}) : Type u_2)) ↦ id (↑j : K)
hi₂ : IsSeparable (↥(adjoin k (insert n (↑s : Set K) \ {n}))) (id n)
⊢ Membership.mem (γ := IntermediateField k K)
    ((fun (t : Set K) ↦
        (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
      (insert n (↑s : Set K) \ {n}))
    n

Tactic:
hi₂

Premises used: Set.Mem, setOf, IsSeparable, Polynomial.Separable, IsCoprime
-- 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 (insert n (↑s : Set K) \ {i}))) (id i)
ne : n ≠ i
⊢ Membership.mem (γ := IntermediateField k K)
    ((fun (t : Set K) ↦
        (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
      (insert n (↑s : Set K) \ {i}))
    n

Tactic:
le_restrictScalars_separableClosure _ (subset_adjoin _ _ ⟨.inl rfl, ne⟩)

Premises used: Set.Mem, IntermediateField.subset_adjoin, le_restrictScalars_separableClosure, And.intro, Or.inl, 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
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
hi₁ : IsTranscendenceBasis k (A := K) fun (j : (↑(insert n (↑s : Set K) \ {n}) : Type u_2)) ↦ id (↑j : K)
hi₂ : IsSeparable (↥(adjoin k (insert n (↑s : Set K) \ {n}))) (id n)
⊢ Membership.mem (γ := IntermediateField k K)
    ((fun (t : Set K) ↦
        (restrictScalars k (L' := ↥(adjoin k t)) (separableClosure (↥(adjoin k t)) K) : IntermediateField k K))
      (insert n (↑s : Set K) \ {n}))
    n

Tactic:
exacts [hi₂, le_restrictScalars_separableClosure _ (subset_adjoin _ _ ⟨.inl rfl, ne⟩)]
-- 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
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
inl :
  CharZero 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
inr :
  ∀ (p : ℕ) (hp : Fact (Nat.Prime p)) (hpk : CharP k p),
    ∃ (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:
obtain _ | ⟨p, hp, hpk⟩ := CharP.exists' k

Premises used: CharP.exists'
-- 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
inst_3 : PerfectField k
inst_4 : Algebra.EssFiniteType k K
h : CharZero k
inl :
  ∀ (s : Finset K) (hs : Eq (α := IntermediateField k K) (adjoin 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:
obtain ⟨s, hs⟩ := IntermediateField.fg_top k K

Premises used: IntermediateField.fg_top