awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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 ⊥
rw₃ rw₄ : K.toSubalgebra = ⊥ ↔ K.toSubalgebra = ⊥
⊢ finrank.{u_1, u_2} F ↥K = 1 ↔ K = ⊥

Tactic:
rw [← toSubalgebra_inj, ← finrank_eq_finrank_subalgebra, Subalgebra.finrank_eq_one_iff,
    bot_toSubalgebra]

Premises used: IntermediateField.bot_toSubalgebra, IntermediateField.finrank_eq_finrank_subalgebra, IntermediateField.toSubalgebra_inj, Subalgebra.finrank_eq_one_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
rw rw₁ : Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊥
⊢ Module.rank F ↥⊥ = 1

Tactic:
rw [rank_eq_one_iff]

Premises used: IntermediateField.rank_eq_one_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
rw rw₁ : Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊥
⊢ finrank.{u_1, u_2} F ↥⊥ = 1

Tactic:
rw [finrank_eq_one_iff]

Premises used: IntermediateField.finrank_eq_one_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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
rw₂ rw₃ : Module.rank (↥⊥) E = Module.rank (↥⊥) E
⊢ Module.rank (↥⊥) E = Module.rank F E

Tactic:
rw [← rank_mul_rank F (⊥ : IntermediateField F E) E, IntermediateField.rank_bot, one_mul]

Premises used: rank_mul_rank, Membership.mem, Subtype, Bot.bot, IntermediateField.rank_bot, one_mul
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ finrank (↥⊥) E = finrank F E

Tactic:
congr(Cardinal.toNat $(rank_bot'))

Premises used: congrArg, Cardinal.toNat, id, IntermediateField.rank_bot', DFunLike.coe
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Module.rank (↥⊤) E = 1

Tactic:
Subalgebra.bot_eq_top_iff_rank_eq_one.mp <| top_le_iff.mp fun x _ ↦ ⟨⟨x, trivial⟩, rfl⟩

Premises used: IntermediateField.copy, trivial, Set.Mem, Subtype.mk, top_le_iff, Exists.intro, Iff.mp, Subalgebra.bot_eq_top_iff_rank_eq_one, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ finrank (↥⊤) E = 1

Tactic:
rank_eq_one_iff_finrank_eq_one.mp IntermediateField.rank_top

Premises used: IntermediateField.rank_top, Module.rank_eq_one_iff_finrank_eq_one, Iff.mp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Module.rank F ↥⊤ = Module.rank F E

Tactic:
rank_top F E

Premises used: IntermediateField.copy, Set.Mem, rank_top
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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 ↥⊤ = finrank F E

Tactic:
finrank_top F E

Premises used: IntermediateField.copy, Set.Mem, finrank_top
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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 = ⊤

Tactic:
⟨?_, (· ▸ IntermediateField.finrank_top)⟩

Premises used: Eq.rec, IntermediateField.finrank_top, Iff.intro, Eq.symm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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
refine : finrank (↥K) E = 1 → K = ⊤
⊢ finrank (↥K) E = 1 ↔ K = ⊤

Tactic:
refine ⟨?_, (· ▸ IntermediateField.finrank_top)⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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 : LE.le.{u_2} (α := Subalgebra (↥K) E) ⊤ ⊥ → ⊤ ≤ K
⊢ finrank (↥K) E = 1 → K = ⊤

Tactic:
rw [← Subalgebra.bot_eq_top_iff_finrank_eq_one, ← top_le_iff, ← top_le_iff]

Premises used: Subalgebra.bot_eq_top_iff_finrank_eq_one, top_le_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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
_ : Membership.mem (γ := IntermediateField F E) ⊤ x → x ∈ K
⊢ Membership.mem (γ := IntermediateField F E) ⊤ x → x ∈ K

Tactic:
_
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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
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)
⊢ x ∈ K

Tactic:
obtain ⟨x, rfl⟩ := @H x IntermediateField.mem_top

Premises used: IntermediateField.mem_top, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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 : ↥K
h :
  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:
x.2

Premises used: Set.Mem, Subtype.property
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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 : ↥K
h :
  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:
exact x.2

Premises used: Subtype.property
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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
rw₁ rw₂ : finrank (↥⊥) E = 1 ↔ finrank (↥⊥) E = 1
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊤ ↔ finrank F E = 1

Tactic:
rw [← IntermediateField.finrank_bot', ← finrank_eq_one_iff_eq_top]

Premises used: IntermediateField.finrank_eq_one_iff_eq_top, IntermediateField.finrank_bot'
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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)

Tactic:
{ toNontrivial := ?_, eq_bot_or_eq_top := ?_ }

Premises used: IsSimpleOrder.mk
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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)
refine_2 : ∀ (a : IntermediateField F E), a = ⊥ ∨ a = ⊤
⊢ IsSimpleOrder.{u_2} (IntermediateField F E)

Tactic:
refine { toNontrivial := ?_, eq_bot_or_eq_top := ?_ }
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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)
⊢ Nontrivial.{u_2} (IntermediateField F E)

Tactic:
⟨⊥, ⊤, fun h ↦ Nat.prime_one_false (bot_eq_top_iff_finrank_eq_one.mp h ▸ hp)⟩

Premises used: Eq.rec, Bot.bot, Nontrivial.mk, IntermediateField.bot_eq_top_iff_finrank_eq_one, Nat.prime_one_false, Exists.intro, Iff.mp, Top.top
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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)
⊢ Nontrivial.{u_2} (IntermediateField F E)

Tactic:
exact ⟨⊥, ⊤, fun h ↦ Nat.prime_one_false (bot_eq_top_iff_finrank_eq_one.mp h ▸ hp)⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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)
K : IntermediateField F E
⊢ K = ⊥ ∨ K = ⊤

Tactic:
simpa [← toSubalgebra_strictMono.apply_eq_bot_iff, ← toSubalgebra_strictMono.apply_eq_top_iff]
      using (Subalgebra.isSimpleOrder_of_finrank_prime _ _ hp).eq_bot_or_eq_top K.toSubalgebra

Premises used: StrictMono.apply_eq_bot_iff, StrictMono.apply_eq_top_iff, IntermediateField.toSubalgebra_strictMono, IsSimpleOrder.eq_bot_or_eq_top, IntermediateField.toSubalgebra
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
⊢ Module.rank F ↥(adjoin F S) = 1 ↔ S ⊆ (↑⊥ : Set E)

Tactic:
Iff.trans rank_eq_one_iff adjoin_eq_bot_iff

Premises used: IntermediateField.adjoin_eq_bot_iff, IntermediateField.rank_eq_one_iff, Iff.trans
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
rw : {α} ⊆ (↑⊥ : Set E) ↔ Membership.mem (γ := IntermediateField F E) ⊥ α
⊢ Module.rank F ↥F⟮α⟯ = 1 ↔ Membership.mem (γ := IntermediateField F E) ⊥ α

Tactic:
rw [rank_adjoin_eq_one_iff]

Premises used: IntermediateField.rank_adjoin_eq_one_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
⊢ {α} ⊆ (↑⊥ : Set E) ↔ Membership.mem (γ := IntermediateField F E) ⊥ α

Tactic:
Set.singleton_subset_iff

Premises used: Set.singleton_subset_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
⊢ {α} ⊆ (↑⊥ : Set E) ↔ Membership.mem (γ := IntermediateField F E) ⊥ α

Tactic:
exact Set.singleton_subset_iff

Premises used: Set.singleton_subset_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
⊢ finrank.{u_1, u_2} F ↥(adjoin F S) = 1 ↔ S ⊆ (↑⊥ : Set E)

Tactic:
Iff.trans finrank_eq_one_iff adjoin_eq_bot_iff

Premises used: IntermediateField.finrank_eq_one_iff, IntermediateField.adjoin_eq_bot_iff, Iff.trans
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
rw : {α} ⊆ (↑⊥ : Set E) ↔ Membership.mem (γ := IntermediateField F E) ⊥ α
⊢ finrank.{u_1, u_2} F ↥F⟮α⟯ = 1 ↔ Membership.mem (γ := IntermediateField F E) ⊥ α

Tactic:
rw [finrank_adjoin_eq_one_iff]

Premises used: IntermediateField.finrank_adjoin_eq_one_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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
h₁ : ∀ (y : E), Membership.mem (γ := IntermediateField F E) ⊥ y ↔ Membership.mem (γ := IntermediateField F E) ⊤ y
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊤

Tactic:
ext y
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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
h₁ : Membership.mem (γ := IntermediateField F E) ⊥ y
⊢ Membership.mem (γ := IntermediateField F E) ⊥ y ↔ Membership.mem (γ := IntermediateField F E) ⊤ y

Tactic:
rw [iff_true_right IntermediateField.mem_top]

Premises used: IntermediateField.mem_top, iff_true_right
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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

Tactic:
rank_adjoin_simple_eq_one_iff.mp (h y)

Premises used: Iff.mp, IntermediateField.rank_adjoin_simple_eq_one_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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

Tactic:
exact rank_adjoin_simple_eq_one_iff.mp (h y)

Premises used: Iff.mp, IntermediateField.rank_adjoin_simple_eq_one_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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
h₁ : ∀ (y : E), Membership.mem (γ := IntermediateField F E) ⊥ y ↔ Membership.mem (γ := IntermediateField F E) ⊤ y
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊤

Tactic:
ext y
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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
h₁ : Membership.mem (γ := IntermediateField F E) ⊥ y
⊢ Membership.mem (γ := IntermediateField F E) ⊥ y ↔ Membership.mem (γ := IntermediateField F E) ⊤ y

Tactic:
rw [iff_true_right IntermediateField.mem_top]

Premises used: IntermediateField.mem_top, iff_true_right
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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

Tactic:
finrank_adjoin_simple_eq_one_iff.mp (h y)

Premises used: Iff.mp, IntermediateField.finrank_adjoin_simple_eq_one_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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

Tactic:
exact finrank_adjoin_simple_eq_one_iff.mp (h y)

Premises used: Iff.mp, IntermediateField.finrank_adjoin_simple_eq_one_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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
⊢ Subsingleton.{u_2 + 1} (IntermediateField F E)

Tactic:
subsingleton_of_bot_eq_top (bot_eq_top_of_rank_adjoin_eq_one h)

Premises used: subsingleton_of_bot_eq_top, IntermediateField.bot_eq_top_of_rank_adjoin_eq_one
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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
⊢ Subsingleton.{u_2 + 1} (IntermediateField F E)

Tactic:
subsingleton_of_bot_eq_top (bot_eq_top_of_finrank_adjoin_eq_one h)

Premises used: IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one, subsingleton_of_bot_eq_top
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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
h₁ : ∀ (x : E), finrank.{u_1, u_2} F ↥F⟮x⟯ = 1
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊤

Tactic:
apply bot_eq_top_of_finrank_adjoin_eq_one

Premises used: IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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
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
⊢ finrank.{u_1, u_2} F ↥F⟮x⟯ = 1

Tactic:
linarith [h x, show 0 < finrank F F⟮x⟯ from finrank_pos]

Premises used: Module.finrank_pos
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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

Tactic:
exact fun x => by linarith [h x, show 0 < finrank F F⟮x⟯ from finrank_pos]
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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
⊢ Subsingleton.{u_2 + 1} (IntermediateField F E)

Tactic:
subsingleton_of_bot_eq_top (bot_eq_top_of_finrank_adjoin_le_one h)

Premises used: subsingleton_of_bot_eq_top, IntermediateField.bot_eq_top_of_finrank_adjoin_le_one
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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 α)
rw₁ rw₂ : Eq (α := F[X]) (minpoly F α) (minpoly F α)
⊢ Eq (α := F[X]) (minpoly F (B := ↥F⟮α⟯) (AdjoinSimple.gen F α)) (minpoly F α)

Tactic:
rw [← minpoly.algebraMap_eq (algebraMap F⟮α⟯ E).injective, AdjoinSimple.algebraMap_gen]

Premises used: Algebra.algebraMap, Membership.mem, Subtype, RingHom.injective, IntermediateField.adjoin, Singleton.singleton, minpoly.algebraMap_eq, IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
a : Eq.{u_2 + 1} (α := E) (↑((aeval (AdjoinSimple.gen F α) : (a : F[X]) → ↥F⟮α⟯) (minpoly F α)) : E) (↑0 : E)
⊢ Eq.{u_2 + 1} (α := ↥F⟮α⟯) ((aeval (AdjoinSimple.gen F α) : (a : F[X]) → ↥F⟮α⟯) (minpoly F α) : ↥F⟮α⟯) (0 : ↥F⟮α⟯)

Tactic:
ext
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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 α : (a : F[X]) → E) (minpoly F α) : E) (0 : E)

Tactic:
minpoly.aeval F α

Premises used: minpoly.aeval
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
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)
⊢ Eq.{u_2 + 1} (α := E) (↑((aeval (AdjoinSimple.gen F α) : (a : F[X]) → ↥F⟮α⟯) (minpoly F α)) : E) (↑0 : E)

Tactic:
convert! minpoly.aeval F α

Premises used: minpoly.aeval
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
rw : (aeval ((algebraMap (↥F⟮α⟯) E : (a : ↥F⟮α⟯) → E) (AdjoinSimple.gen F α)) : F[X] →ₐ[F] E)
| aeval α

Tactic:
rw [← AdjoinSimple.algebraMap_gen F α]

Premises used: IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
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)
⊢ 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:
conv in aeval α => rw [← AdjoinSimple.algebraMap_gen F α]

Premises used: Polynomial.aeval, IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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 ((algebraMap (↥F⟮α⟯) E : (a : ↥F⟮α⟯) → E) (AdjoinSimple.gen F α)) : F[X] →ₐ[F] E) : (a : F[X]) → E)
        (minpoly F α) :
      E)

Tactic:
(aeval_algebraMap_apply E (AdjoinSimple.gen F α) _).symm

Premises used: Set.Mem, IntermediateField.AdjoinSimple.gen, IntermediateField.adjoin, Eq.symm, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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 ((algebraMap (↥F⟮α⟯) E : (a : ↥F⟮α⟯) → E) (AdjoinSimple.gen F α)) : F[X] →ₐ[F] E) : (a : F[X]) → E)
        (minpoly F α) :
      E)

Tactic:
exact (aeval_algebraMap_apply E (AdjoinSimple.gen F α) _).symm

Premises used: IntermediateField.AdjoinSimple.gen, Eq.symm, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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 α) ⋯
⊢ Fact (Irreducible (M := F[X]) (minpoly F α))

Tactic:
haveI := Fact.mk (minpoly.irreducible h)
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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⟮α⟯)
right :
  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⟮α⟯)
⊢ 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⟮α⟯)

Tactic:
constructor
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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.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⟮α⟯)

Tactic:
RingHom.injective f

Premises used: Set.Mem, MonoidHomClass.toMonoidHom, RingHom.injective, RingHomClass.toRingHom, RingHom.codRestrict
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
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.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⟮α⟯)

Tactic:
exact RingHom.injective f

Premises used: RingHom.injective