awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : (↑S : Type u_2)), F⟮(↑i : E)⟯) x
s : Finset (↑S : Type u_2)
hx' : Membership.mem (γ := IntermediateField F E) (⨆ i ∈ s, F⟮(↑i : E)⟯) x
refine :
  LE.le (α := IntermediateField F E) (⨆ i ∈ s, F⟮(↑i : E)⟯)
    (adjoin F (↑(Finset.image (Subtype.val (p := fun (x : E) ↦ x ∈ S)) s) : Set E))
refine₁ :
  ∀ (i : (↑S : Type u_2)) (i_1 : i ∈ s),
    {(↑i : E)} ⊆ (↑(adjoin F (Subtype.val (p := fun (x : E) ↦ x ∈ S) '' (↑s : Set { x : E // x ∈ S }))) : Set E)
⊢ ∃ (T : Finset E), (↑T : Set E) ⊆ S ∧ Membership.mem (γ := IntermediateField F E) (adjoin F (↑T : Set E)) x
have refine₂ : ∀ (i : (↑S : Type u_2)) (h : i ∈ s),
  (↑i : E) ∈ (↑(adjoin F (Subtype.val (p := fun (x : E) ↦ x ∈ S) '' (↑s : Set { x : E // x ∈ S }))) : Set E)
Tactic: classical
  refine ⟨s.image Subtype.val, by simp, SetLike.le_def.mp ?_ hx'⟩
  simp_rw [Finset.coe_image, iSup_le_iff, adjoin_le_iff]
  rintro _ h _ rfl
  exact subset_adjoin F _ ⟨_, h, rfl⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
⊢ Module.rank F ↥K = 1 ↔ K = ⊥
have rw : Module.rank F ↥K = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
Tactic: rw [← toSubalgebra_inj, ← rank_eq_rank_subalgebra, Subalgebra.rank_eq_one_iff,
    bot_toSubalgebra]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
rw : Module.rank F ↥K = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
⊢ Module.rank F ↥K = 1 ↔ K = ⊥
have rw₁ : Module.rank F ↥K.toSubalgebra = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
Tactic: rw [← toSubalgebra_inj, ← rank_eq_rank_subalgebra, Subalgebra.rank_eq_one_iff,
    bot_toSubalgebra]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
rw : Module.rank F ↥K = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
rw₁ : Module.rank F ↥K.toSubalgebra = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
⊢ Module.rank F ↥K = 1 ↔ K = ⊥
have rw₂ : K.toSubalgebra = ⊥ ↔ K.toSubalgebra = toSubalgebra ⊥
Tactic: rw [← toSubalgebra_inj, ← rank_eq_rank_subalgebra, Subalgebra.rank_eq_one_iff,
    bot_toSubalgebra]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
rw : Module.rank F ↥K = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
rw₁ : Module.rank F ↥K.toSubalgebra = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
rw₂ : K.toSubalgebra = ⊥ ↔ K.toSubalgebra = toSubalgebra ⊥
⊢ Module.rank F ↥K = 1 ↔ K = ⊥
have rw₃ : K.toSubalgebra = ⊥ ↔ K.toSubalgebra = ⊥
Tactic: rw [← toSubalgebra_inj, ← rank_eq_rank_subalgebra, Subalgebra.rank_eq_one_iff,
    bot_toSubalgebra]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
⊢ finrank.{u_1, u_2} F ↥K = 1 ↔ K = ⊥
have rw : finrank.{u_1, u_2} F ↥K = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
Tactic: rw [← toSubalgebra_inj, ← finrank_eq_finrank_subalgebra, Subalgebra.finrank_eq_one_iff,
    bot_toSubalgebra]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
rw : finrank.{u_1, u_2} F ↥K = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
⊢ finrank.{u_1, u_2} F ↥K = 1 ↔ K = ⊥
have rw₁ : finrank.{u_1, u_2} F ↥K.toSubalgebra = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
Tactic: rw [← toSubalgebra_inj, ← finrank_eq_finrank_subalgebra, Subalgebra.finrank_eq_one_iff,
    bot_toSubalgebra]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
rw : finrank.{u_1, u_2} F ↥K = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
rw₁ : finrank.{u_1, u_2} F ↥K.toSubalgebra = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
⊢ finrank.{u_1, u_2} F ↥K = 1 ↔ K = ⊥
have rw₂ : K.toSubalgebra = ⊥ ↔ K.toSubalgebra = toSubalgebra ⊥
Tactic: rw [← toSubalgebra_inj, ← finrank_eq_finrank_subalgebra, Subalgebra.finrank_eq_one_iff,
    bot_toSubalgebra]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
rw : finrank.{u_1, u_2} F ↥K = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
rw₁ : finrank.{u_1, u_2} F ↥K.toSubalgebra = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
rw₂ : K.toSubalgebra = ⊥ ↔ K.toSubalgebra = toSubalgebra ⊥
⊢ finrank.{u_1, u_2} F ↥K = 1 ↔ K = ⊥
have rw₃ : K.toSubalgebra = ⊥ ↔ K.toSubalgebra = ⊥
Tactic: rw [← toSubalgebra_inj, ← finrank_eq_finrank_subalgebra, Subalgebra.finrank_eq_one_iff,
    bot_toSubalgebra]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Module.rank F ↥⊥ = 1
have rw : Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊥
Tactic: rw [rank_eq_one_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ finrank.{u_1, u_2} F ↥⊥ = 1
have rw : Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊥
Tactic: rw [finrank_eq_one_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Module.rank (↥⊥) E = Module.rank F E
have rw : Module.rank (↥⊥) E = Module.rank F ↥⊥ * Module.rank (↥⊥) E
Tactic: rw [← rank_mul_rank F (⊥ : IntermediateField F E) E, IntermediateField.rank_bot, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
rw : Module.rank (↥⊥) E = Module.rank F ↥⊥ * Module.rank (↥⊥) E
⊢ Module.rank (↥⊥) E = Module.rank F E
have rw₁ : Module.rank (↥⊥) E = 1 * Module.rank (↥⊥) E
Tactic: rw [← rank_mul_rank F (⊥ : IntermediateField F E) E, IntermediateField.rank_bot, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
rw : Module.rank (↥⊥) E = Module.rank F ↥⊥ * Module.rank (↥⊥) E
rw₁ : Module.rank (↥⊥) E = 1 * Module.rank (↥⊥) E
⊢ Module.rank (↥⊥) E = Module.rank F E
have rw₂ : Module.rank (↥⊥) E = Module.rank (↥⊥) E
Tactic: rw [← rank_mul_rank F (⊥ : IntermediateField F E) E, IntermediateField.rank_bot, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
⊢ finrank (↥K) E = 1 ↔ K = ⊤
have refine : finrank (↥K) E = 1 → K = ⊤
Tactic: refine ⟨?_, (· ▸ IntermediateField.finrank_top)⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
⊢ finrank (↥K) E = 1 → K = ⊤
have rw : LE.le.{u_2} (α := Subalgebra (↥K) E) ⊤ ⊥ → ⊤ ≤ K
Tactic: rw [← Subalgebra.bot_eq_top_iff_finrank_eq_one, ← top_le_iff, ← top_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
H : LE.le.{u_2} (α := Subalgebra (↥K) E) ⊤ ⊥
x : E
h : Membership.mem (γ := IntermediateField F E) ⊤ x
⊢ x ∈ K
have obtain : ∀ (x : ↥K),
  Membership.mem (α := E) (γ := IntermediateField F E) ⊤
      ((AlgHom.toRingHom (Algebra.ofId (↥K) E) : (a : ↥K) → E) x : E) →
    Membership.mem (α := E) K ((AlgHom.toRingHom (Algebra.ofId (↥K) E) : (a : ↥K) → E) x : E)
Tactic: obtain ⟨x, rfl⟩ := @H x IntermediateField.mem_top
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊤ ↔ finrank F E = 1
have rw : Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊤ ↔ finrank (↥⊥) E = 1
Tactic: rw [← IntermediateField.finrank_bot', ← finrank_eq_one_iff_eq_top]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
rw : Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊤ ↔ finrank (↥⊥) E = 1
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊤ ↔ finrank F E = 1
have rw₁ : finrank (↥⊥) E = 1 ↔ finrank (↥⊥) E = 1
Tactic: rw [← IntermediateField.finrank_bot', ← finrank_eq_one_iff_eq_top]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
hp : Nat.Prime (finrank F E)
⊢ IsSimpleOrder.{u_2} (IntermediateField F E)
have refine_1 : Nontrivial.{u_2} (IntermediateField F E)
Tactic: refine { toNontrivial := ?_, eq_bot_or_eq_top := ?_ }
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
hp : Nat.Prime (finrank F E)
refine_1 : Nontrivial.{u_2} (IntermediateField F E)
⊢ IsSimpleOrder.{u_2} (IntermediateField F E)
have refine_2 : ∀ (a : IntermediateField F E), a = ⊥ ∨ a = ⊤
Tactic: refine { toNontrivial := ?_, eq_bot_or_eq_top := ?_ }
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
⊢ Module.rank F ↥F⟮α⟯ = 1 ↔ Membership.mem (γ := IntermediateField F E) ⊥ α
have rw : {α} ⊆ (↑⊥ : Set E) ↔ Membership.mem (γ := IntermediateField F E) ⊥ α
Tactic: rw [rank_adjoin_eq_one_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
⊢ finrank.{u_1, u_2} F ↥F⟮α⟯ = 1 ↔ Membership.mem (γ := IntermediateField F E) ⊥ α
have rw : {α} ⊆ (↑⊥ : Set E) ↔ Membership.mem (γ := IntermediateField F E) ⊥ α
Tactic: rw [finrank_adjoin_eq_one_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊤
have h₁ : ∀ (y : E), Membership.mem (γ := IntermediateField F E) ⊥ y ↔ Membership.mem (γ := IntermediateField F E) ⊤ y
Tactic: ext y
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1
y : E
⊢ Membership.mem (γ := IntermediateField F E) ⊥ y ↔ Membership.mem (γ := IntermediateField F E) ⊤ y
have h₁ : Membership.mem (γ := IntermediateField F E) ⊥ y
Tactic: rw [iff_true_right IntermediateField.mem_top]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : ∀ (x : E), finrank.{u_1, u_2} F ↥F⟮x⟯ = 1
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊤
have h₁ : ∀ (y : E), Membership.mem (γ := IntermediateField F E) ⊥ y ↔ Membership.mem (γ := IntermediateField F E) ⊤ y
Tactic: ext y
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : ∀ (x : E), finrank.{u_1, u_2} F ↥F⟮x⟯ = 1
y : E
⊢ Membership.mem (γ := IntermediateField F E) ⊥ y ↔ Membership.mem (γ := IntermediateField F E) ⊤ y
have h₁ : Membership.mem (γ := IntermediateField F E) ⊥ y
Tactic: rw [iff_true_right IntermediateField.mem_top]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : ∀ (x : E), finrank.{u_1, u_2} F ↥F⟮x⟯ ≤ 1
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊤
have h₁ : ∀ (x : E), finrank.{u_1, u_2} F ↥F⟮x⟯ = 1
Tactic: apply bot_eq_top_of_finrank_adjoin_eq_one
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : ∀ (x : E), finrank.{u_1, u_2} F ↥F⟮x⟯ ≤ 1
x : E
⊢ finrank.{u_1, u_2} F ↥F⟮x⟯ = 1
have linarith : finrank.{u_1, u_2} F ↥F⟮x⟯ < 1 →
  -1 + (HAdd.hAdd (α := ℤ) (↑(finrank.{u_1, u_2} F ↥F⟮x⟯) : ℤ) 1 - 1) +
      (HAdd.hAdd (α := ℤ) 0 1 - (↑(finrank.{u_1, u_2} F ↥F⟮x⟯) : ℤ)) =
    0
Tactic: linarith [h x, show 0 < finrank F F⟮x⟯ from finrank_pos]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : ∀ (x : E), finrank.{u_1, u_2} F ↥F⟮x⟯ ≤ 1
x : E
linarith :
  finrank.{u_1, u_2} F ↥F⟮x⟯ < 1 →
    -1 + (HAdd.hAdd (α := ℤ) (↑(finrank.{u_1, u_2} F ↥F⟮x⟯) : ℤ) 1 - 1) +
        (HAdd.hAdd (α := ℤ) 0 1 - (↑(finrank.{u_1, u_2} F ↥F⟮x⟯) : ℤ)) =
      0
⊢ finrank.{u_1, u_2} F ↥F⟮x⟯ = 1
have linarith₁ : 1 < finrank.{u_1, u_2} F ↥F⟮x⟯ →
  -1 + (HAdd.hAdd (α := ℤ) 1 1 - (↑(finrank.{u_1, u_2} F ↥F⟮x⟯) : ℤ)) +
      HSub.hSub (α := ℤ) (↑(finrank.{u_1, u_2} F ↥F⟮x⟯) : ℤ) 1 =
    0
Tactic: linarith [h x, show 0 < finrank F F⟮x⟯ from finrank_pos]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
⊢ Eq (α := F[X]) (minpoly F (B := ↥F⟮α⟯) (AdjoinSimple.gen F α)) (minpoly F α)
have rw : Eq (α := F[X]) (minpoly F (B := E) ((algebraMap (↥F⟮α⟯) E : (a : ↥F⟮α⟯) → E) (AdjoinSimple.gen F α) : E)) (minpoly F α)
Tactic: rw [← minpoly.algebraMap_eq (algebraMap F⟮α⟯ E).injective, AdjoinSimple.algebraMap_gen]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
rw :
  Eq (α := F[X]) (minpoly F (B := E) ((algebraMap (↥F⟮α⟯) E : (a : ↥F⟮α⟯) → E) (AdjoinSimple.gen F α) : E))
    (minpoly F α)
⊢ Eq (α := F[X]) (minpoly F (B := ↥F⟮α⟯) (AdjoinSimple.gen F α)) (minpoly F α)
have rw₁ : Eq (α := F[X]) (minpoly F α) (minpoly F α)
Tactic: rw [← minpoly.algebraMap_eq (algebraMap F⟮α⟯ E).injective, AdjoinSimple.algebraMap_gen]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
⊢ Eq.{u_2 + 1} (α := ↥F⟮α⟯) ((aeval (AdjoinSimple.gen F α) : (a : F[X]) → ↥F⟮α⟯) (minpoly F α) : ↥F⟮α⟯) (0 : ↥F⟮α⟯)
have a : Eq.{u_2 + 1} (α := E) (↑((aeval (AdjoinSimple.gen F α) : (a : F[X]) → ↥F⟮α⟯) (minpoly F α)) : E) (↑0 : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
⊢ Eq.{u_2 + 1} (α := E) (↑((aeval (AdjoinSimple.gen F α) : (a : F[X]) → ↥F⟮α⟯) (minpoly F α)) : E) (↑0 : E)
have h : Eq.{u_2 + 1} (α := E) ((↑((aeval (AdjoinSimple.gen F α) : (a : F[X]) → ↥F⟮α⟯) (minpoly F α)) : E) : E)
  ((aeval α : (a : F[X]) → E) (minpoly F α) : E)
Tactic: convert! minpoly.aeval F α
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
| aeval α
have rw : (aeval ((algebraMap (↥F⟮α⟯) E : (a : ↥F⟮α⟯) → E) (AdjoinSimple.gen F α)) : F[X] →ₐ[F] E)
Tactic: rw [← AdjoinSimple.algebraMap_gen F α]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
⊢ Eq.{u_2 + 1} (α := E) ((↑((aeval (AdjoinSimple.gen F α) : (a : F[X]) → ↥F⟮α⟯) (minpoly F α)) : E) : E)
    ((aeval α : (a : F[X]) → E) (minpoly F α) : E)
have h : Eq.{u_2 + 1} (α := E) ((↑((aeval (AdjoinSimple.gen F α) : (a : F[X]) → ↥F⟮α⟯) (minpoly F α)) : E) : E)
  (((aeval ((algebraMap (↥F⟮α⟯) E : (a : ↥F⟮α⟯) → E) (AdjoinSimple.gen F α)) : F[X] →ₐ[F] E) : (a : F[X]) → E)
      (minpoly F α) :
    E)
Tactic: conv in aeval α => rw [← AdjoinSimple.algebraMap_gen F α]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := AdjoinRoot (minpoly F α)) (β := ↥F⟮α⟯)
    (⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯) :
      (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
have this : Fact (Irreducible (M := F[X]) (minpoly F α))
Tactic: haveI := Fact.mk (minpoly.irreducible h)
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := AdjoinRoot (minpoly F α)) (β := ↥F⟮α⟯)
    (⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯) :
      (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
have left : Function.Injective.{u_1 + 1, u_2 + 1} (α := AdjoinRoot (minpoly F α)) (β := ↥F⟮α⟯)
  (⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) sorry) :
    (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
left :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := AdjoinRoot (minpoly F α)) (β := ↥F⟮α⟯)
    (⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯) :
      (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := AdjoinRoot (minpoly F α)) (β := ↥F⟮α⟯)
    (⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯) :
      (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
have right : Function.Surjective.{u_1 + 1, u_2 + 1} (α := AdjoinRoot (minpoly F α)) (β := ↥F⟮α⟯)
  (⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) sorry) :
    (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this_1 : Fact (Irreducible (M := F[X]) (minpoly F α))
this : toSubfield F⟮α⟯ ≤ (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange
x : ↥F⟮α⟯
⊢ ∃ (a : AdjoinRoot (minpoly F α)),
    ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯ :
            AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F α)) ↥F⟮α⟯) :
          (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
        a =
      x
have obtain : ∀ (y : AdjoinRoot (minpoly F α))
  (hy : (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f : (a : AdjoinRoot (minpoly F α)) → E) y = (↑x : E)),
  ∃ (a : AdjoinRoot (minpoly F α)),
    ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) sorry :
            AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F α)) ↥F⟮α⟯) :
          (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
        a =
      x
Tactic: obtain ⟨y, hy⟩ := this (Subtype.mem x)
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := AdjoinRoot (minpoly F α)) (β := ↥F⟮α⟯)
    (⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯) :
      (a : AdjoinRoot (minpoly F α)) → ↥F⟮α⟯)
have right : toSubfield F⟮α⟯ ≤ (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange
Tactic: suffices F⟮α⟯.toSubfield ≤ RingHom.fieldRange (F⟮α⟯.toSubfield.subtype.comp f) by
          intro x
          obtain ⟨y, hy⟩ := this (Subtype.mem x)
          exact ⟨y, Subtype.ext hy⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
⊢ toSubfield F⟮α⟯ ≤ (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange
have right : ∀ (x : E) (hx : Membership.mem (γ := Set E) (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x),
  x ∈ (↑(RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange : Set E)
Tactic: refine Subfield.closure_le.mpr (Set.union_subset (fun x hx => ?_) ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
f : RingHom.{u_1, u_2} (AdjoinRoot (minpoly F α)) ↥F⟮α⟯ :=
  AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯) : F →+* ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯
this : Fact (Irreducible (M := F[X]) (minpoly F α))
right :
  ∀ (x : E) (hx : Membership.mem (γ := Set E) (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x),
    x ∈ (↑(RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange : Set E)
⊢ toSubfield F⟮α⟯ ≤ (RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange
have right₁ : {α} ⊆ (↑(RingHom.comp (Subfield.subtype (toSubfield F⟮α⟯)) f).fieldRange : Set E)
Tactic: refine Subfield.closure_le.mpr (Set.union_subset (fun x hx => ?_) ?_)