awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)}
⊢ ∃ (i : ι),
    (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
      IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
have obtain : ∀ (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)),
  ∃ (i : ι),
    (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
      IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
Tactic: obtain ⟨F, ⟨hF₀, hFa⟩, hFmin⟩ :
      ∃ F ∈ S, ∀ G : MvPolynomial ι k, G ≠ 0 → G.aeval a = 0 → totalDegree F ≤ totalDegree G := by
    suffices S.Nonempty from
      ⟨totalDegree.argminOn S this, totalDegree.argminOn_mem ..,
        fun _ h₁ h₂ ↦ totalDegree.argminOn_le S ⟨h₁, h₂⟩⟩
    suffices ¬ AlgebraicIndependent k a by simpa [S, algebraicIndependent_iff, and_comm] using this
    intro h
    refine h.transcendental_adjoin (i := n) (s := {n}ᶜ) (by simp) ?_
    have : a '' {n}ᶜ = Set.range (ι := {i // i ≠ n}) (a ·) := by aesop
    convert! ha'.isAlgebraic.isAlgebraic _
-- 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)
⊢ ∃ (i : ι),
    (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
      IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
have hFirr : Irreducible F
Tactic: have hFirr : Irreducible F := irreducible_of_forall_totalDegree_le hFmin hF₀ hFa
-- 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 : ι),
    (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
      IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
have obtain : ∀ (i : ι) (σ : ι →₀ ℕ) (hσ : σ ∈ F.support) (hi : ¬p ∣ (σ : (a : ι) → ℕ) i),
  ∃ (i : ι),
    (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
      IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
Tactic: obtain ⟨i, σ, hσ, hi⟩ := exists_mem_support_not_dvd_of_forall_totalDegree_le p hp H hFmin hF₀ hFa
-- 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
⊢ ∃ (i : ι),
    (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
      IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
have hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
Tactic: have hσi : σ i ≠ 0 := by aesop
-- 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 : ℕ)
⊢ ∃ (i : ι),
    (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
      IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
have alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Tactic: have alg := isAlgebraic_of_mem_vars_of_forall_totalDegree_le hFmin hFa i <|
    (mem_vars_iff_mem_support i).mpr ⟨σ, hσ, by simpa⟩
-- 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)
⊢ ∃ (i : ι),
    (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
      IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
have Hi : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (x : { x : ι // x ≠ i }) ↦ a (↑x : ι)
Tactic: have Hi := ha'.of_isAlgebraic_adjoin_image_compl _ i _ alg
-- 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 : ι)
⊢ ∃ (i : ι),
    (IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (j : { j : ι // j ≠ i }) ↦ a (↑j : ι)) ∧
      IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
have refine : IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
Tactic: refine ⟨i, Hi, ?_⟩
-- 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}ᶜ)
⊢ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
have hF₁irr : Irreducible (M := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (F.toPolynomialAdjoinImageCompl a i)
Tactic: have hF₁irr := irreducible_toPolynomialAdjoinImageCompl hFirr i Hi.1
-- 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)
⊢ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
have this : UniqueFactorizationMonoid.{u_2} ↥(Algebra.adjoin k (a '' {i}ᶜ))
Tactic: have := (AlgebraicIndepOn.aevalEquiv (s := {i}ᶜ) Hi.1).uniqueFactorizationMonoid inferInstance
-- 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 : UniqueFactorizationMonoid.{u_2} ↥(Algebra.adjoin k (a '' {i}ᶜ))
⊢ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
have coeff_ne : Ne (α := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i))
  0
Tactic: have coeff_ne := coeff_toPolynomialAdjoinImageCompl_ne_zero hFmin σ hσ i hσi
-- 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 : 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 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))
Tactic: 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
-- 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
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)
have contrapose : ∀ (Hsep : ¬IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)),
  Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
Tactic: contrapose coeff_ne with Hsep
Cleared hypotheses: coeff_ne
-- 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 : 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)
⊢ Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
have this₁ : CharP.{u_2} (↥k') p
Tactic: have : CharP k' p := (expChar_of_injective_algebraMap (algebraMap k k').injective p).casesOn
    (fun e ↦ (e rfl).elim) (fun _ _ _ ↦ ‹_›) hp.ne_one
-- 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_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
⊢ Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
have obtain : ∀ (g : Polynomial ↥k') (hg : Irreducible g)
  (eq :
    Eq (α := Polynomial ↥k') ((Polynomial.expand (↥k') p : (a : Polynomial ↥k') → Polynomial ↥k') g : Polynomial ↥k')
      (minpoly (↥k') (a i) : Polynomial ↥k')),
  Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
Tactic: obtain ⟨g, hg, eq⟩ := (((minpoly k' (a i)).separable_or p (minpoly.irreducible
    (isAlgebraic_iff_isIntegral.mp <| isAlgebraic_adjoin_iff.mpr alg))).resolve_left Hsep).2