awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
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)
⊢ False
have hi₃ : IsSeparable (↥(adjoin k (insert n (↑s : Set K) \ {i}))) (id i)
Tactic: rw [Set.image_id] at hi₂
Cleared hypotheses: hi₂
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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)
⊢ False
have 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}))
Tactic: refine not_lt_iff_le_imp_ge.mpr (Hs hi₁) (SetLike.lt_iff_le_and_exists.mpr ⟨?_, n, ?_, hn⟩)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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}))
⊢ False
have 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
Tactic: refine not_lt_iff_le_imp_ge.mpr (Hs hi₁) (SetLike.lt_iff_le_and_exists.mpr ⟨?_, n, ?_, hn⟩)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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)
⊢ 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}))
have 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)
Tactic: rw [separableClosure_le_separableClosure_iff, adjoin_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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)
⊢ x ∈
    (↑(restrictScalars k (L' := ↥(adjoin k (insert n (↑s : Set K) \ {i})))
          (separableClosure (↥(adjoin k (insert n (↑s : Set K) \ {i}))) K)) :
      Set K)
have 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)
Tactic: obtain rfl | ne := eq_or_ne x i
Cleared hypotheses: i, hi₁, hi₂
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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)
⊢ x ∈
    (↑(restrictScalars k (L' := ↥(adjoin k (insert n (↑s : Set K) \ {i})))
          (separableClosure (↥(adjoin k (insert n (↑s : Set K) \ {i}))) K)) :
      Set K)
have 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)
Tactic: obtain rfl | ne := eq_or_ne x i
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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)
⊢ 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
have 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
Tactic: obtain rfl | ne := eq_or_ne n i
Cleared hypotheses: i, hi₁, hi₂
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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
⊢ 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
have 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
Tactic: obtain rfl | ne := eq_or_ne n i
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain _ | ⟨p, hp, hpk⟩ := CharP.exists' k
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain _ | ⟨p, hp, hpk⟩ := CharP.exists' k
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨s, hs⟩ := IntermediateField.fg_top k K
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
⊢ Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
have rw : Algebra.IsIntegral (↥⊤) K
Tactic: rw [← isAlgebraic_adjoin_iff_top, hs, Algebra.isAlgebraic_iff_isIntegral]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
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
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
have this : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
Tactic: have : Algebra.IsAlgebraic (Algebra.adjoin k (s : Set K)) K := by
      rw [← isAlgebraic_adjoin_iff_top, hs, Algebra.isAlgebraic_iff_isIntegral]
      exact Algebra.isIntegral_of_surjective topEquiv.surjective
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.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
have inl : ∀ (t : Set K) (hts : t ⊆ (↑s : Set K))
  (ht : IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t))),
  ∃ (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 ⟨t, hts, ht⟩ := exists_isTranscendenceBasis_subset (R := k) (s : Set K)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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
s : Finset K
hs : Eq (α := IntermediateField k K) (adjoin k (↑s : Set K)) ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k (↑s : Set K))) K
t : Set K
hts : t ⊆ (↑s : Set K)
ht : IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ t }) k (Subtype.val (p := fun (x : K) ↦ x ∈ t))
⊢ ∃ (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
have inl : ∀ (t : Finset K) (hts : (↑t : Set K) ⊆ (↑s : Set K))
  (ht :
    IsTranscendenceBasis.{u_2, u_1, u_2} (ι := { x : K // x ∈ (↑t : Set K) }) k
      (Subtype.val (p := fun (x : K) ↦ x ∈ (↑t : 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: lift t to Finset K using s.finite_toSet.subset hts
Cleared hypotheses: t, hts, ht