awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + y • β⟯ (α + y • β)
⊢ {α, β} ⊆ (↑F⟮α + x • β⟯ : Set E)
have αyβ_in_K₁ : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)
Tactic: simp only [← heq] at αyβ_in_K
Cleared hypotheses: αyβ_in_K
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)
⊢ {α, β} ⊆ (↑F⟮α + x • β⟯ : Set E)
have β_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β - (α + y • β))
Tactic: have β_in_K := sub_mem αxβ_in_K αyβ_in_K
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)
β_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β - (α + y • β))
⊢ α + x • β - (α + y • β) = (x - y) • β
have rw : α + x • β - (α + y • β) = x • β - y • β
Tactic: rw [sub_smul]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)
β_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β - (α + y • β))
⊢ {α, β} ⊆ (↑F⟮α + x • β⟯ : Set E)
have β_in_K₁ : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ ((x - y) • β)
Tactic: rw [show (α + x • β) - (α + y • β) = (x - y) • β by rw [sub_smul]; abel1] at β_in_K
Cleared hypotheses: β_in_K
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)
β_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ ((x - y) • β)
⊢ {α, β} ⊆ (↑F⟮α + x • β⟯ : Set E)
have β_in_K₁ : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ ((x - y)⁻¹ • (x - y) • β)
Tactic: replace β_in_K := smul_mem _ β_in_K (x := (x - y)⁻¹)
Cleared hypotheses: β_in_K
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)
β_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ ((x - y)⁻¹ • (x - y) • β)
⊢ {α, β} ⊆ (↑F⟮α + x • β⟯ : Set E)
have β_in_K₁ : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ β
Tactic: rw [smul_smul, inv_mul_eq_div, div_self (sub_ne_zero.2 hneq), one_smul] at β_in_K
Cleared hypotheses: β_in_K
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)
β_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ β
⊢ {α, β} ⊆ (↑F⟮α + x • β⟯ : Set E)
have α_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ α
Tactic: have α_in_K : α ∈ F⟮α + x • β⟯ := by
      convert! ← sub_mem αxβ_in_K (smul_mem _ β_in_K)
      apply add_sub_cancel_right
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ LE.le (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α, β⟯
have h : Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ (α + x • β)
Tactic: rw [adjoin_simple_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ (α + x • β)
have α_in_Fαβ : Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ α
Tactic: have α_in_Fαβ : α ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert α {β})
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
α_in_Fαβ : Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ α
⊢ Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ (α + x • β)
have β_in_Fαβ : Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ β
Tactic: have β_in_Fαβ : β ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert_of_mem α rfl)
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
⊢ ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
have inl : ∀ (F_inf : IsEmpty.{u_1 + 1} (Fintype F)), ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
Tactic: rcases isEmpty_or_nonempty (Fintype F) with (F_inf | ⟨⟨F_finite⟩⟩)
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
inl : ∀ (F_inf : IsEmpty.{u_1 + 1} (Fintype F)), ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
⊢ ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
have inr : ∀ (F_finite : Fintype F), ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
Tactic: rcases isEmpty_or_nonempty (Fintype F) with (F_inf | ⟨⟨F_finite⟩⟩)
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
⊢ ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
have base : P ⊥
Tactic: have base : P ⊥ := ⟨0, adjoin_zero⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β : E
hK : P K
⊢ P (IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮β⟯)
have obtain : ∀ (α : E) (hK : F⟮α⟯ = K), P (IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮β⟯)
Tactic: obtain ⟨α, hK⟩ := hK
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β α : E
hK : F⟮α⟯ = K
⊢ P (IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮β⟯)
have rw : P F⟮α, β⟯
Tactic: rw [← hK, adjoin_simple_adjoin_simple]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β α : E
hK : F⟮α⟯ = K
⊢ P F⟮α, β⟯
have haveI : ∀ (this : Infinite F), P F⟮α, β⟯
Tactic: haveI : Infinite F := isEmpty_fintype.mp F_inf
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β α : E
hK : F⟮α⟯ = K
this : Infinite F
⊢ P F⟮α, β⟯
have obtain : ∀ (γ : E) (hγ : Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯), P F⟮α, β⟯
Tactic: obtain ⟨γ, hγ⟩ := primitive_element_inf_aux F α β
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
base : P ⊥
⊢ ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
have ih : ∀ (K : IntermediateField F E) (x : E), P K → P (IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
Tactic: have ih : ∀ (K : IntermediateField F E) (x : E), P K → P (K⟮x⟯.restrictScalars F) := by
      intro K β hK
      obtain ⟨α, hK⟩ := hK
      rw [← hK, adjoin_simple_adjoin_simple]
      haveI : Infinite F := isEmpty_fintype.mp F_inf
      obtain ⟨γ, hγ⟩ := primitive_element_inf_aux F α β
      exact ⟨γ, hγ.symm⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
⊢ IsAlgebraic F α
have inr : ∀
  (this :
    ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_3 : Field E] [inst_4 : Algebra F E] {α : E} {m n : ℕ}
      (hneq : m ≠ n) (heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯) (hmn : m < n), IsAlgebraic F α)
  (hmn : ¬m < n), IsAlgebraic F α
Tactic: wlog hmn : m < n
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
inr :
  ∀
    (this :
      ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_3 : Field E] [inst_4 : Algebra F E] {α : E} {m n : ℕ}
        (hneq : m ≠ n) (heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯) (hmn : m < n), IsAlgebraic F α)
    (hmn : ¬m < n), IsAlgebraic F α
⊢ IsAlgebraic F α
have wlog : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_3 : Field E] [inst_4 : Algebra F E] {α : E} {m n : ℕ}
  (hneq : m ≠ n) (heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯) (hmn : m < n), IsAlgebraic F α
Tactic: wlog hmn : m < n
Cleared hypotheses: α, m, n, hneq, heq
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
⊢ IsAlgebraic F α
have pos : ∀ (hm : m = 0), IsAlgebraic F α
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
pos : ∀ (hm : m = 0), IsAlgebraic F α
⊢ IsAlgebraic F α
have neg : ∀ (hm : ¬m = 0), IsAlgebraic F α
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : m = 0
⊢ IsAlgebraic F α
have heq₁ : Eq (α := IntermediateField F E) F⟮HPow.hPow (β := ℕ) α 0⟯ F⟮α ^ n⟯
Tactic: rw [hm] at heq hmn
Cleared hypotheses: heq, hmn, hm
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : m = 0
heq₁ : Eq (α := IntermediateField F E) F⟮HPow.hPow (β := ℕ) α 0⟯ F⟮α ^ n⟯
⊢ IsAlgebraic F α
have hmn₁ : 0 < n
Tactic: rw [hm] at heq hmn
Cleared hypotheses: heq, hmn, hm
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮HPow.hPow (β := ℕ) α 0⟯ F⟮α ^ n⟯
hmn : 0 < n
hm : m = 0
⊢ IsAlgebraic F α
have heq₁ : Eq (α := IntermediateField F E) ⊥ F⟮α ^ n⟯
Tactic: simp only [pow_zero, adjoin_one] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
hmn : 0 < n
hm : m = 0
heq : Eq (α := IntermediateField F E) ⊥ F⟮α ^ n⟯
⊢ IsAlgebraic F α
have pos : ∀ (y : F) (h : (algebraMap F E : (a : F) → E) y = α ^ n), IsAlgebraic F α
Tactic: obtain ⟨y, h⟩ := mem_bot.1 (heq.symm ▸ mem_adjoin_simple_self F (α ^ n))
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
hmn : 0 < n
hm : m = 0
heq : Eq (α := IntermediateField F E) ⊥ F⟮α ^ n⟯
y : F
h : (algebraMap F E : (a : F) → E) y = α ^ n
⊢ IsAlgebraic F α
have pos : Eq.{u_2 + 1} (α := E)
  ((aeval α : (a : F[X]) → E) (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) y : F[X])) : E)
  (0 : E)
Tactic: refine ⟨X ^ n - C y, X_pow_sub_C_ne_zero hmn y, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
⊢ IsAlgebraic F α
have neg : ∀ (r s : F[X])
  (h :
    α ^ m =
      HDiv.hDiv (α := E) (β := E) ((aeval (α ^ n) : (a : F[X]) → E) r : E) ((aeval (α ^ n) : (a : F[X]) → E) s : E)),
  IsAlgebraic F α
Tactic: obtain ⟨r, s, h⟩ := (mem_adjoin_simple_iff F _).1 (heq ▸ mem_adjoin_simple_self F (α ^ m))
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
h :
  α ^ m = HDiv.hDiv (α := E) (β := E) ((aeval (α ^ n) : (a : F[X]) → E) r : E) ((aeval (α ^ n) : (a : F[X]) → E) s : E)
⊢ IsAlgebraic F α
have pos : ∀ (hzero : Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)), IsAlgebraic F α
Tactic: by_cases hzero : aeval (α ^ n) s = 0
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
h :
  α ^ m = HDiv.hDiv (α := E) (β := E) ((aeval (α ^ n) : (a : F[X]) → E) r : E) ((aeval (α ^ n) : (a : F[X]) → E) s : E)
pos : ∀ (hzero : Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)), IsAlgebraic F α
⊢ IsAlgebraic F α
have neg : ∀ (hzero : ¬Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)), IsAlgebraic F α
Tactic: by_cases hzero : aeval (α ^ n) s = 0
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
h :
  α ^ m = HDiv.hDiv (α := E) (β := E) ((aeval (α ^ n) : (a : F[X]) → E) r : E) ((aeval (α ^ n) : (a : F[X]) → E) s : E)
hzero : Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)
⊢ IsAlgebraic F α
have h₁ : α = 0
Tactic: simp only [hzero, div_zero, pow_eq_zero_iff hm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
h :
  α ^ m = HDiv.hDiv (α := E) (β := E) ((aeval (α ^ n) : (a : F[X]) → E) r : E) ((aeval (α ^ n) : (a : F[X]) → E) s : E)
hzero : ¬Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)
⊢ IsAlgebraic F α
have hm₁ : 0 < m
Tactic: replace hm : 0 < m := Nat.pos_of_ne_zero hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  α ^ m = HDiv.hDiv (α := E) (β := E) ((aeval (α ^ n) : (a : F[X]) → E) r : E) ((aeval (α ^ n) : (a : F[X]) → E) s : E)
hzero : ¬Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)
hm : 0 < m
⊢ IsAlgebraic F α
have h₁ : HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
    ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
  0
Tactic: rw [eq_div_iff hzero, ← sub_eq_zero] at h
Cleared hypotheses: h, hzero, hm
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hzero : ¬Eq.{u_2 + 1} (α := E) ((aeval (α ^ n) : (a : F[X]) → E) s : E) (0 : E)
hm : 0 < m
⊢ IsAlgebraic F α
have hzero₁ : s ≠ 0
Tactic: replace hzero : s ≠ 0 := by rintro rfl; simp only [map_zero, not_true_eq_false] at hzero
Cleared hypotheses: hzero
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
⊢ IsAlgebraic F α
have neg : f ≠ 0
Tactic: refine ⟨f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
neg : f ≠ 0
⊢ IsAlgebraic F α
have neg₁ : Eq.{u_2 + 1} (α := E) ((aeval α : (a : F[X]) → E) f : E) (0 : E)
Tactic: refine ⟨f, ?_, ?_⟩