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
ι : 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 (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
have eq₁ : 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))
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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 : UniqueFactorizationMonoid.{u_2} ↥(Algebra.adjoin k (a '' {i}ᶜ))
coeff_ne :
  Ne (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
⊢ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
have open : ∀
  (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))),
  IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
Tactic: open scoped algebraAdjoinAdjoin in
  have hF₂irr := (hF₁irr.isPrimitive fun h ↦ coeff_ne <| Polynomial.coeff_eq_zero_of_natDegree_lt <|
    h.trans_lt <| Nat.pos_iff_ne_zero.2 hσi).irreducible_iff_irreducible_map_fraction_map
    (K := k').1 hF₁irr
  contrapose coeff_ne with Hsep
  have : CharP k' p := (expChar_of_injective_algebraMap (algebraMap k k').injective p).casesOn
    (fun e ↦ (e rfl).elim) (fun _ _ _ ↦ ‹_›) hp.ne_one
  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
  replace eq := congr(Polynomial.coeff $eq (σ i))
  rwa [← minpoly.eq_of_irreducible hF₂irr ((Polynomial.aeval_map_algebraMap ..).trans
    (aeval_toPolynomialAdjoinImageCompl_eq_zero hFa i)), Polynomial.coeff_mul_C,
    Polynomial.coeff_expand hp.pos, if_neg hi, eq_mul_inv_iff_mul_eq₀
    (by simpa using hF₂irr.ne_zero), zero_mul, eq_comm,
    Polynomial.coeff_map, map_eq_zero_iff _ (FaithfulSMul.algebraMap_injective ..)] at eq
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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 : ι),
    (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)
have 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)
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₁)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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}ᶜ
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
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 := ⋯ }
⊢ ∃ (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)
have this : 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
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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 : ι),
    (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
      Algebra.IsSeparable (↥(adjoin k (a '' {i}ᶜ))) K
have 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
Tactic: have ⟨i, hi⟩ := exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow p hp H n ha'
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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
have refine : Algebra.IsSeparable (↥(adjoin k (a '' {i}ᶜ))) K
Tactic: refine ⟨i, hi.1, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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)
⊢ Algebra.IsSeparable (↥(adjoin k (a '' {i}ᶜ))) K
have rw : Set.range a ⊆
  (↑(restrictScalars k (L' := ↥(adjoin k (a '' {i}ᶜ))) (separableClosure (↥(adjoin k (a '' {i}ᶜ))) K)) : Set K)
Tactic: rw [← separableClosure.eq_top_iff, ← (restrictScalars_injective k).eq_iff,
    restrictScalars_top, eq_top_iff, ← ha, adjoin_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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 : ι
⊢ a x ∈ (↑(restrictScalars k (L' := ↥(adjoin k (a '' {i}ᶜ))) (separableClosure (↥(adjoin k (a '' {i}ᶜ))) K)) : Set K)
have 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)
Tactic: obtain rfl | ne := eq_or_ne x i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
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)
⊢ a x ∈ (↑(restrictScalars k (L' := ↥(adjoin k (a '' {i}ᶜ))) (separableClosure (↥(adjoin k (a '' {i}ᶜ))) K)) : Set K)
have inr : ∀ (ne : x ≠ i),
  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
-- 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),
    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 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
Tactic: have ⟨s, hs, Hs⟩ := exists_finset_maximalFor_isTranscendenceBasis_separableClosure 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
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
have refine : ∀ (n : K) (hn : ¬IsSeparable (↥(adjoin k (↑s : Set K))) n), False
Tactic: refine ⟨s, hs, ⟨fun n ↦ of_not_not fun hn ↦ ?_⟩⟩
-- 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
⊢ False
have hns : n ∉ s
Tactic: have hns : n ∉ s := fun h ↦ hn (le_restrictScalars_separableClosure _ (subset_adjoin _ _ h))
-- 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
⊢ False
have 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
Tactic: have ⟨i, hi₁, hi₂⟩ := exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow'
    p hp (a := id) H s n hs hns