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
inst_3 : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
n : ℕ
zero : ∃ (L : IntermediateField F E), FiniteDimensional.{u_1, u_2} F ↥L ∧ 0 < finrank.{u_1, u_2} F ↥L
succ :
  ∀ (n : ℕ) (ih : ∃ (L : IntermediateField F E), FiniteDimensional.{u_1, u_2} F ↥L ∧ n < finrank.{u_1, u_2} F ↥L),
    ∃ (L : IntermediateField F E), FiniteDimensional.{u_1, u_2} F ↥L ∧ n + 1 < finrank.{u_1, u_2} F ↥L
⊢ ∃ (L : IntermediateField F E), FiniteDimensional.{u_1, u_2} F ↥L ∧ n < finrank.{u_1, u_2} F ↥L

Tactic:
induction n with
  | zero => exact ⟨⊥, Subalgebra.finite_bot, finrank_pos⟩
  | succ n ih =>
    obtain ⟨L, fin, hn⟩ := ih
    obtain ⟨x, hx⟩ : ∃ x : E, x ∉ L := by
      contrapose! hnfd
      rw [show L = ⊤ from eq_top_iff.2 fun x _ ↦ hnfd x] at fin
      exact topEquiv.toLinearEquiv.finiteDimensional
    let L' := L ⊔ F⟮x⟯
    haveI := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (R := F) x)
    refine ⟨L', inferInstance, by_contra fun h ↦ ?_⟩
    have h1 : L = L' := eq_of_le_of_finrank_le le_sup_left ((not_lt.1 h).trans hn)
    have h2 : F⟮x⟯ ≤ L' := le_sup_right
    exact hx <| (h1.symm ▸ h2) <| mem_adjoin_simple_self F x
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : IsIntegral K x
rw : ∃ (c : ℕ), finrank K L = c * finrank.{u, u_3} K ↥K⟮x⟯
⊢ natDegree (minpoly K x) ∣ finrank K L

Tactic:
rw [dvd_iff_exists_eq_mul_left, ← IntermediateField.adjoin.finrank hx]

Premises used: IntermediateField.adjoin.finrank, dvd_iff_exists_eq_mul_left
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : IsIntegral K x
h : finrank K L = finrank (↥K⟮x⟯) L * finrank.{u, u_3} K ↥K⟮x⟯
⊢ ∃ (c : ℕ), finrank K L = c * finrank.{u, u_3} K ↥K⟮x⟯

Tactic:
use finrank K⟮x⟯ L

Premises used: Membership.mem, Subtype, IntermediateField.adjoin, Singleton.singleton, Module.finrank
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : IsIntegral K x
h : finrank K L = finrank.{u, u_3} K ↥K⟮x⟯ * finrank (↥K⟮x⟯) L
h₁ h₂ : finrank K L = finrank K L
⊢ finrank K L = finrank (↥K⟮x⟯) L * finrank.{u, u_3} K ↥K⟮x⟯

Tactic:
rw [mul_comm, finrank_mul_finrank]

Premises used: Module.finrank_mul_finrank, mul_comm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hi : Irreducible f
hs : Splits (Polynomial.map (algebraMap K L) f)
⊢ f.degree ≠ 0

Tactic:
have := hi.degree_pos.ne'
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hi : Irreducible f
hs : Splits (Polynomial.map (algebraMap K L) f)
this : f.degree ≠ 0
⊢ degree (Polynomial.map (algebraMap K L) f) ≠ 0

Tactic:
rw [← f.degree_map (algebraMap K L)] at this

Premises used: Algebra.algebraMap, Polynomial.degree_map
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hi : Irreducible f
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
obtain : ∀ (x : L) (hx : eval x (Polynomial.map (algebraMap K L) f) = 0), f.natDegree ∣ finrank K L
⊢ f.natDegree ∣ finrank K L

Tactic:
obtain ⟨x, hx⟩ := hs.exists_eval_eq_zero this

Premises used: Polynomial.Splits.exists_eval_eq_zero
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hi : Irreducible f
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : eval x (Polynomial.map (algebraMap K L) f) = 0
⊢ Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)

Tactic:
rw [eval_map_algebraMap] at hx

Premises used: Polynomial.eval_map_algebraMap
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hi : Irreducible f
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
⊢ f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (minpoly K x)

Tactic:
have key := minpoly.Irreducible.eq_minpoly hi hx
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hi : Irreducible f
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (minpoly K x)
⊢ f ≠ 0

Tactic:
replace hi := hi.ne_zero
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (minpoly K x)
hi : f ≠ 0
rw : natDegree (minpoly K x) ∣ finrank K L
⊢ f.natDegree ∣ finrank K L

Tactic:
rw [key, natDegree_C_mul (leadingCoeff_ne_zero.mpr hi)]

Premises used: Iff.mpr, Polynomial.natDegree_C_mul, Polynomial.leadingCoeff_ne_zero
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (minpoly K x)
hi : f ≠ 0
hx₁ : IsIntegral K x
⊢ natDegree (minpoly K x) ∣ finrank K L

Tactic:
apply minpoly.degree_dvd

Premises used: minpoly.degree_dvd
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (minpoly K x)
hi : f ≠ 0
hx₁ : Ne (α := K[X]) (minpoly K x) 0
⊢ IsIntegral K x

Tactic:
rw [← minpoly.ne_zero_iff]

Premises used: minpoly.ne_zero_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (minpoly K x)
hi : f ≠ 0
hx₁ : ∀ (hi : Eq (α := K[X]) (minpoly K x) 0), f = 0
⊢ Ne (α := K[X]) (minpoly K x) 0

Tactic:
contrapose hi
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
f : K[X]
hs : Splits (Polynomial.map (algebraMap K L) f)
this : degree (Polynomial.map (algebraMap K L) f) ≠ 0
x : L
hx : Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) f : L) (0 : L)
key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (minpoly K x)
hi : Eq (α := K[X]) (minpoly K x) 0
hx₁ :
  ∀ (key : f = HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff : K[X]) (0 : K[X]))
    (hi : Eq (α := K[X]) (minpoly K x) 0), f = 0
hx₂ hx₃ hx₄ hx₅ : ∀ (key : f = 0) (hi : Eq (α := K[X]) (minpoly K x) 0), f = 0
⊢ f = 0

Tactic:
rwa [hi, mul_zero] at key

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic.{u, u_3} K ↥(t i)
isAlgebraic : ∀ (x : ↥(⨆ (i : ι), t i)), IsAlgebraic K x
⊢ Algebra.IsAlgebraic.{u, u_3} K ↥(⨆ (i : ι), t i)

Tactic:
constructor
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic.{u, u_3} K ↥(t i)
x : L
hx : Membership.mem (γ := IntermediateField K L) (⨆ (i : ι), t i) x
isAlgebraic :
  ∀ (s : Finset ((i : ι) × ↥(t i)))
    (hx_1 : Membership.mem (γ := IntermediateField K L) (⨆ i ∈ s, K⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(t i))) : L)⟯) x),
    IsAlgebraic K (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := IntermediateField K L) (⨆ (i : ι), t i) x) x hx)
⊢ IsAlgebraic K (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := IntermediateField K L) (⨆ (i : ι), t i) x) x hx)

Tactic:
obtain ⟨s, hx⟩ := exists_finset_of_mem_supr' hx

Premises used: IntermediateField.exists_finset_of_mem_supr'
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic.{u, u_3} K ↥(t i)
x : L
hx_1 : Membership.mem (γ := IntermediateField K L) (⨆ (i : ι), t i) x
s : Finset ((i : ι) × ↥(t i))
hx : Membership.mem (γ := IntermediateField K L) (⨆ i ∈ s, K⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(t i))) : L)⟯) x
isAlgebraic :
  IsAlgebraic K
    (Subtype.mk (p := fun (x : L) ↦
      Membership.mem (γ := IntermediateField K L) (⨆ i ∈ s, K⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(t i))) : L)⟯) x) x hx)
⊢ IsAlgebraic K (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := IntermediateField K L) (⨆ (i : ι), t i) x) x hx_1)

Tactic:
rw [isAlgebraic_iff, Subtype.coe_mk, ← Subtype.coe_mk (p := (· ∈ _)) x hx, ← isAlgebraic_iff]

Premises used: Subtype.coe_mk, IntermediateField.isAlgebraic_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic.{u, u_3} K ↥(t i)
x : L
hx_1 : Membership.mem (γ := IntermediateField K L) (⨆ (i : ι), t i) x
s : Finset ((i : ι) × ↥(t i))
hx : Membership.mem (γ := IntermediateField K L) (⨆ i ∈ s, K⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(t i))) : L)⟯) x
⊢ ∀ (i : (i : ι) × ↥(t i)), FiniteDimensional.{u, u_3} K ↥K⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(t i))) : L)⟯

Tactic:
haveI : ∀ i : Σ i, t i, FiniteDimensional K K⟮(i.2 : L)⟯ := fun ⟨i, x⟩ ↦
    adjoin.finiteDimensional (isIntegral_iff.1 (Algebra.IsIntegral.isIntegral x))
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic.{u, u_3} K ↥(t i)
x : L
hx_1 : Membership.mem (γ := IntermediateField K L) (⨆ (i : ι), t i) x
s : Finset ((i : ι) × ↥(t i))
hx : Membership.mem (γ := IntermediateField K L) (⨆ i ∈ s, K⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(t i))) : L)⟯) x
this : ∀ (i : (i : ι) × ↥(t i)), FiniteDimensional.{u, u_3} K ↥K⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(t i))) : L)⟯
⊢ IsAlgebraic K
    (Subtype.mk (p := fun (x : L) ↦
      Membership.mem (γ := IntermediateField K L) (⨆ i ∈ s, K⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(t i))) : L)⟯) x) x hx)

Tactic:
apply IsAlgebraic.of_finite

Premises used: IsAlgebraic.of_finite
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
S : Set L
hS : ∀ x ∈ S, IsIntegral K x
rw : Algebra.IsAlgebraic.{u, u_3} K ↥(⨆ (i : (↑S : Type u_3)), K⟮(↑i : L)⟯)
⊢ Algebra.IsAlgebraic.{u, u_3} K ↥(adjoin K S)

Tactic:
rw [← biSup_adjoin_simple, ← iSup_subtype'']

Premises used: iSup_subtype'', IntermediateField.biSup_adjoin_simple
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
S : Set L
hS : ∀ x ∈ S, IsIntegral K x
⊢ Algebra.IsAlgebraic.{u, u_3} K ↥(⨆ (i : (↑S : Type u_3)), K⟮(↑i : L)⟯)

Tactic:
isAlgebraic_iSup fun x ↦ isAlgebraic_adjoin_simple (hS x x.2)

Premises used: Set.Mem, IntermediateField.isAlgebraic_adjoin_simple, IntermediateField.isAlgebraic_iSup, Subtype.val, Subtype.property
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
S : Set L
hS : ∀ x ∈ S, IsIntegral K x
⊢ Algebra.IsAlgebraic.{u, u_3} K ↥(⨆ (i : (↑S : Type u_3)), K⟮(↑i : L)⟯)

Tactic:
exact isAlgebraic_iSup fun x ↦ isAlgebraic_adjoin_simple (hS x x.2)
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
S : Set L
inst_3 : Finite.{u_3 + 1} (↑S : Type u_3)
hS : ∀ x ∈ S, IsIntegral K x
rw : FiniteDimensional.{u, u_3} K ↥(⨆ (i : (↑S : Type u_3)), K⟮(↑i : L)⟯)
⊢ FiniteDimensional.{u, u_3} K ↥(adjoin K S)

Tactic:
rw [← biSup_adjoin_simple, ← iSup_subtype'']

Premises used: iSup_subtype'', IntermediateField.biSup_adjoin_simple
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
S : Set L
inst_3 : Finite.{u_3 + 1} (↑S : Type u_3)
hS : ∀ x ∈ S, IsIntegral K x
⊢ ∀ (x : (↑S : Type u_3)), FiniteDimensional.{u, u_3} K ↥K⟮(↑x : L)⟯

Tactic:
haveI (x : S) := adjoin.finiteDimensional (hS x.1 x.2)
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
S : Set L
inst_3 : Finite.{u_3 + 1} (↑S : Type u_3)
hS : ∀ x ∈ S, IsIntegral K x
this : ∀ (x : (↑S : Type u_3)), FiniteDimensional.{u, u_3} K ↥K⟮(↑x : L)⟯
⊢ FiniteDimensional.{u, u_3} K ↥(⨆ (i : (↑S : Type u_3)), K⟮(↑i : L)⟯)

Tactic:
finiteDimensional_iSup_of_finite

Premises used: Set.Mem, IntermediateField.finiteDimensional_iSup_of_finite
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
S : Set L
inst_3 : Finite.{u_3 + 1} (↑S : Type u_3)
hS : ∀ x ∈ S, IsIntegral K x
this : ∀ (x : (↑S : Type u_3)), FiniteDimensional.{u, u_3} K ↥K⟮(↑x : L)⟯
⊢ FiniteDimensional.{u, u_3} K ↥(⨆ (i : (↑S : Type u_3)), K⟮(↑i : L)⟯)

Tactic:
exact finiteDimensional_iSup_of_finite

Premises used: IntermediateField.finiteDimensional_iSup_of_finite
-- 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 α
x : K
rw :
  x ∈ aroots (minpoly F (B := ↥F⟮α⟯) (AdjoinSimple.gen F α)) K ↔
    Membership.mem (α := K) (aroots (minpoly F α) K) ((Equiv.refl K : (a : K) → K) x : K)
rw₁ : x ∈ aroots (minpoly F α) K ↔ Membership.mem (α := K) (aroots (minpoly F α) K) ((Equiv.refl K : (a : K) → K) x : K)
rw₂ rw₃ : x ∈ aroots (minpoly F α) K ↔ x ∈ aroots (minpoly F α) K
⊢ x ∈ aroots (minpoly F (adjoin.powerBasis h).gen) K ↔
    Membership.mem (α := K) (aroots (minpoly F α) K) ((Equiv.refl K : (a : K) → K) x : K)

Tactic:
rw [adjoin.powerBasis_gen, minpoly_gen, Equiv.refl_apply]

Premises used: Equiv.refl_apply, IntermediateField.minpoly_gen, IntermediateField.adjoin.powerBasis_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
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
x : { x : K // x ∈ aroots (minpoly F α) K }
rw : Eq.{u + 1} (α := K) ((aeval (↑x : K) : (a : F[X]) → K) (minpoly F α) : K) (0 : K)
⊢ Eq.{u + 1} (α := K) ((aeval (↑x : K) : (a : F[X]) → K) (minpoly F (adjoin.powerBasis h).gen) : K) (0 : K)

Tactic:
rw [adjoin.powerBasis_gen, minpoly_gen]

Premises used: IntermediateField.minpoly_gen, IntermediateField.adjoin.powerBasis_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
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
x : { x : K // x ∈ aroots (minpoly F α) K }
⊢ Eq.{u + 1} (α := K) ((aeval (↑x : K) : (a : F[X]) → K) (minpoly F α) : K) (0 : K)

Tactic:
(mem_aroots.mp x.2).2

Premises used: And.right, Iff.mp, Polynomial.mem_aroots, 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
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
x : { x : K // x ∈ aroots (minpoly F α) K }
⊢ Eq.{u + 1} (α := K) ((aeval (↑x : K) : (a : F[X]) → K) (minpoly F α) : K) (0 : K)

Tactic:
exact (mem_aroots.mp x.2).2

Premises used: And.right, Iff.mp, Polynomial.mem_aroots, 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
α : E
K : Type u
inst_3 : Field K
inst_4 : Algebra F K
h : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Splits (Polynomial.map (algebraMap F K) (minpoly F α))
x : Fintype (AlgHom.{u_1, u_2, u} F (↥F⟮α⟯) K) := fintypeOfAlgHomAdjoinIntegral F h
rw : (adjoin.powerBasis h).dim = natDegree (minpoly F α)
h_sep₁ : IsSeparable F (adjoin.powerBasis h).gen
h_splits₁ : Splits (Polynomial.map (algebraMap F K) (minpoly F (adjoin.powerBasis h).gen))
⊢ Nat.card (AlgHom.{u_1, u_2, u} F (↥F⟮α⟯) K) = natDegree (minpoly F α)

Tactic:
rw [Nat.card_eq_fintype_card, AlgHom.card_of_powerBasis]

Premises used: AlgHom.card_of_powerBasis, Nat.card_eq_fintype_card
-- 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 α
h_sep : IsSeparable F α
h_splits : Splits (Polynomial.map (algebraMap F K) (minpoly F α))
x : Fintype (AlgHom.{u_1, u_2, u} F (↥F⟮α⟯) K) := fintypeOfAlgHomAdjoinIntegral F h
⊢ (adjoin.powerBasis h).dim = natDegree (minpoly F α)

Tactic:
simp only [IsSeparable, adjoin.powerBasis_dim, adjoin.powerBasis_gen, minpoly_gen, h_splits]

Premises used: IntermediateField.minpoly_gen, IntermediateField.adjoin.powerBasis_gen, IsSeparable, IntermediateField.adjoin.powerBasis_dim
-- 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 α
h_sep : IsSeparable F α
h_splits : Splits (Polynomial.map (algebraMap F K) (minpoly F α))
x : Fintype (AlgHom.{u_1, u_2, u} F (↥F⟮α⟯) K) := fintypeOfAlgHomAdjoinIntegral F h
h_sep₁ : Separable (minpoly F α)
⊢ IsSeparable F (adjoin.powerBasis h).gen

Tactic:
simp only [IsSeparable, adjoin.powerBasis_dim, adjoin.powerBasis_gen, minpoly_gen, h_splits]

Premises used: IntermediateField.minpoly_gen, IntermediateField.adjoin.powerBasis_gen, IsSeparable, IntermediateField.adjoin.powerBasis_dim
-- 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 α
h_sep : IsSeparable F α
h_splits : Splits (Polynomial.map (algebraMap F K) (minpoly F α))
x : Fintype (AlgHom.{u_1, u_2, u} F (↥F⟮α⟯) K) := fintypeOfAlgHomAdjoinIntegral F h
⊢ Splits (Polynomial.map (algebraMap F K) (minpoly F (adjoin.powerBasis h).gen))

Tactic:
simp only [IsSeparable, adjoin.powerBasis_dim, adjoin.powerBasis_gen, minpoly_gen, h_splits]

Premises used: IntermediateField.minpoly_gen, IntermediateField.adjoin.powerBasis_gen, IsSeparable, IntermediateField.adjoin.powerBasis_dim
-- 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 α
h_sep : IsSeparable F α
h_splits : Splits (Polynomial.map (algebraMap F K) (minpoly F α))
x : Fintype (AlgHom.{u_1, u_2, u} F (↥F⟮α⟯) K) := fintypeOfAlgHomAdjoinIntegral F h
⊢ Separable (minpoly F α)

Tactic:
h_sep

Premises used: IsSeparable
-- 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 α
h_sep : IsSeparable F α
h_splits : Splits (Polynomial.map (algebraMap F K) (minpoly F α))
x : Fintype (AlgHom.{u_1, u_2, u} F (↥F⟮α⟯) K) := fintypeOfAlgHomAdjoinIntegral F h
⊢ Separable (minpoly F α)

Tactic:
exact h_sep
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
⊢ f.natDegree ≠ 0

Tactic:
have hf' : natDegree f ≠ 0 :=
    fun e ↦ not_irreducible_C (f.coeff 0) (eq_C_of_natDegree_eq_zero e ▸ hf)
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
⊢ Fact (Irreducible f)

Tactic:
have := Fact.mk hf
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u
inst : Field K
f g : K[X]
hfm : f.Monic
hgm : g.Monic
hf : Irreducible f
hg :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = f →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) g)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hf' : f.natDegree ≠ 0
this : Fact (Irreducible f)
e : g.natDegree = 0
apply :
  Irreducible (M := (↥K⟮root f⟯)[X])
    ((C : (a : ↥K⟮root f⟯) → (↥K⟮root f⟯)[X])
        (HSub.hSub (α := ↥K⟮root f⟯) (coeff (Polynomial.map (algebraMap K ↥K⟮root f⟯) g) 0)
          (AdjoinSimple.gen K (root f))) :
      (↥K⟮root f⟯)[X])
⊢ False

Tactic:
apply not_irreducible_C ((g.map (algebraMap _ _)).coeff 0 - AdjoinSimple.gen K (root f))

Premises used: Algebra.algebraMap, IntermediateField.AdjoinSimple.gen, HSub.hSub, Polynomial.coeff, AdjoinRoot.root, Polynomial.map, Polynomial.not_irreducible_C, OfNat.ofNat