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
α : E
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
n : ℕ
rw : Membership.mem (α := E) (↑K : Set E) ((algebraMap (↥K) E : (a : ↥K) → E) (coeff (minpoly (↥K) α) n) : E)
⊢ g.coeff n ∈ (↑K : Set E)

Tactic:
rw [coeff_map]

Premises used: Polynomial.coeff_map
-- 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
n : ℕ
⊢ Membership.mem (α := E) (↑K : Set E) ((algebraMap (↥K) E : (a : ↥K) → E) (coeff (minpoly (↥K) α) n) : E)

Tactic:
apply Subtype.mem

Premises used: Subtype.mem
-- 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
⊢ K' ≤ K

Tactic:
have hsub : K' ≤ K := by
    refine adjoin_le_iff.mpr fun x ↦ ?_
    rw [Finset.mem_coe, mem_coeffs_iff]
    rintro ⟨n, -, rfl⟩
    rw [coeff_map]
    apply Subtype.mem
-- 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K
hp : Eq (α := E) ((aeval α : (a : (↥K')[X]) → E) (g.toSubring K'.toSubring ⋯) : E) (0 : E)
⊢ Dvd.dvd (α := (↥K')[X]) (minpoly (↥K') α) (g.toSubring K'.toSubring ⋯)

Tactic:
apply minpoly.dvd

Premises used: minpoly.dvd
-- 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K
hp : eval α (Polynomial.map (R := ↥K') (algebraMap (↥K') E) (g.toSubring K'.toSubring ⋯)) = 0
⊢ Eq (α := E) ((aeval α : (a : (↥K')[X]) → E) (g.toSubring K'.toSubring ⋯) : E) (0 : E)

Tactic:
rw [aeval_def, eval₂_eq_eval_map]

Premises used: Polynomial.aeval_def, Polynomial.eval₂_eq_eval_map
-- 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K
hp : eval α g = 0
⊢ eval α (Polynomial.map (R := ↥K') (algebraMap (↥K') E) (g.toSubring K'.toSubring ⋯)) = 0

Tactic:
erw [g.map_toSubring K'.toSubring]

Premises used: Subalgebra.toSubring, Polynomial.map_toSubring, 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
α : E
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K
hp : Eq (α := E) ((aeval α : (a : (↥K)[X]) → E) (minpoly (↥K) α) : E) (0 : E)
⊢ eval α g = 0

Tactic:
rw [eval_map_algebraMap]

Premises used: Polynomial.eval_map_algebraMap
-- 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K
⊢ Eq (α := E) ((aeval α : (a : (↥K)[X]) → E) (minpoly (↥K) α) : E) (0 : E)

Tactic:
minpoly.aeval K α

Premises used: Set.Mem, Membership.mem, Subtype, 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K
⊢ Eq (α := E) ((aeval α : (a : (↥K)[X]) → E) (minpoly (↥K) α) : E) (0 : E)

Tactic:
exact minpoly.aeval K α

Premises used: Membership.mem, Subtype, 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K
⊢ Dvd.dvd (α := (↥K')[X]) (minpoly (↥K') α) (g.toSubring K'.toSubring ⋯)

Tactic:
have dvd_g : minpoly K' α ∣ g.toSubring K'.toSubring (subset_adjoin F _) := by
    apply minpoly.dvd
    rw [aeval_def, eval₂_eq_eval_map]
    erw [g.map_toSubring K'.toSubring]
    rw [eval_map_algebraMap]
    exact minpoly.aeval K α
-- 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K_1 : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K_1) (algebraMap (↥K_1) E) (minpoly (↥K_1) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K_1
dvd_g : Dvd.dvd (α := (↥K')[X]) (minpoly (↥K') α) (g.toSubring K'.toSubring ⋯)
K : IntermediateField F E
⊢ finrank.{u_2, u_2} ↥K ↥(↥K)⟮α⟯ = natDegree (R := ↥K) (minpoly (↥K) α)

Tactic:
have := adjoin.finrank (.of_finite K α)
-- 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K_1 : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K_1) (algebraMap (↥K_1) E) (minpoly (↥K_1) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K_1
dvd_g : Dvd.dvd (α := (↥K')[X]) (minpoly (↥K') α) (g.toSubring K'.toSubring ⋯)
K : IntermediateField F E
this : finrank.{u_2, u_2} ↥K ↥(↥K)⟮α⟯ = natDegree (R := ↥K) (minpoly (↥K) α)
⊢ finrank.{u_2, u_2} ↥K ↥⊤ = natDegree (R := ↥K) (minpoly (↥K) α)

Tactic:
rw [adjoin_eq_top_of_adjoin_eq_top F hprim] at this

Premises used: IntermediateField.adjoin_eq_top_of_adjoin_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
α : E
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K_1 : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K_1) (algebraMap (↥K_1) E) (minpoly (↥K_1) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K_1
dvd_g : Dvd.dvd (α := (↥K')[X]) (minpoly (↥K') α) (g.toSubring K'.toSubring ⋯)
K : IntermediateField F E
this : finrank.{u_2, u_2} ↥K ↥⊤ = natDegree (R := ↥K) (minpoly (↥K) α)
⊢ finrank (↥K) E = natDegree (R := ↥K) (minpoly (↥K) α)

Tactic:
simp_all
-- 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K
dvd_g : Dvd.dvd (α := (↥K')[X]) (minpoly (↥K') α) (g.toSubring K'.toSubring ⋯)
⊢ ∀ (K : IntermediateField F E), finrank (↥K) E = natDegree (R := ↥K) (minpoly (↥K) α)

Tactic:
have finrank_eq : ∀ K : IntermediateField F E, finrank K E = natDegree (minpoly K α) := by
    intro K
    have := adjoin.finrank (.of_finite K α)
    rw [adjoin_eq_top_of_adjoin_eq_top F hprim] at this
    simp_all
-- 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K
dvd_g : Dvd.dvd (α := (↥K')[X]) (minpoly (↥K') α) (g.toSubring K'.toSubring ⋯)
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = natDegree (R := ↥K) (minpoly (↥K) α)
⊢ K' = K

Tactic:
eq_of_le_of_finrank_le' hsub ?_

Premises used: IntermediateField.eq_of_le_of_finrank_le'
-- 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K
dvd_g : Dvd.dvd (α := (↥K')[X]) (minpoly (↥K') α) (g.toSubring K'.toSubring ⋯)
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = natDegree (R := ↥K) (minpoly (↥K) α)
refine : finrank (↥K') E ≤ finrank (↥K) E
⊢ K' = K

Tactic:
refine eq_of_le_of_finrank_le' hsub ?_

Premises used: IntermediateField.eq_of_le_of_finrank_le'
-- 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K
dvd_g : Dvd.dvd (α := (↥K')[X]) (minpoly (↥K') α) (g.toSubring K'.toSubring ⋯)
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = natDegree (R := ↥K) (minpoly (↥K) α)
simp_rw : natDegree (R := ↥K') (minpoly (↥K') α) ≤ natDegree (R := ↥K) (minpoly (↥K) α)
⊢ finrank (↥K') E ≤ finrank (↥K) E

Tactic:
simp_rw [finrank_eq]
-- 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K
dvd_g : Dvd.dvd (α := (↥K')[X]) (minpoly (↥K') α) (g.toSubring K'.toSubring ⋯)
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = natDegree (R := ↥K) (minpoly (↥K) α)
⊢ natDegree (R := ↥K') (minpoly (↥K') α) ≤ natDegree (R := ↥K') (g.toSubring K'.toSubring ⋯)

Tactic:
natDegree_le_of_dvd dvd_g
      ((g.monic_toSubring _ _).mpr <| (minpoly.monic <| .of_finite K α).map _).ne_zero

Premises used: Iff.mpr, Polynomial.monic_toSubring, minpoly.monic, Membership.mem, Subtype, Polynomial.natDegree_le_of_dvd, IsIntegral.of_finite, Polynomial.Monic.map, Polynomial.Monic.ne_zero
-- 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K
dvd_g : Dvd.dvd (α := (↥K')[X]) (minpoly (↥K') α) (g.toSubring K'.toSubring ⋯)
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = natDegree (R := ↥K) (minpoly (↥K) α)
h : natDegree (R := ↥K) (minpoly (↥K) α) = natDegree (R := ↥K') (g.toSubring K'.toSubring ⋯)
⊢ natDegree (R := ↥K') (minpoly (↥K') α) ≤ natDegree (R := ↥K) (minpoly (↥K) α)

Tactic:
convert!
    natDegree_le_of_dvd dvd_g
      ((g.monic_toSubring _ _).mpr <| (minpoly.monic <| .of_finite K α).map _).ne_zero using 1

Premises used: Iff.mpr, Polynomial.monic_toSubring, minpoly.monic, Membership.mem, Subtype, Polynomial.natDegree_le_of_dvd, IsIntegral.of_finite, Polynomial.Monic.map, Polynomial.Monic.ne_zero
-- 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
inst_3 : FiniteDimensional F E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
K : IntermediateField F E
g : E[X] := Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)
K' : IntermediateField F E := adjoin F (↑g.coeffs : Set E)
hsub : K' ≤ K
dvd_g : Dvd.dvd (α := (↥K')[X]) (minpoly (↥K') α) (g.toSubring K'.toSubring ⋯)
finrank_eq : ∀ (K : IntermediateField F E), finrank (↥K) E = natDegree (R := ↥K) (minpoly (↥K) α)
h : natDegree (R := ↥K) (minpoly (↥K) α) = g.natDegree
h₁ h₂ : natDegree (R := ↥K) (minpoly (↥K) α) = natDegree (R := ↥K) (minpoly (↥K) α)
⊢ natDegree (R := ↥K) (minpoly (↥K) α) = natDegree (R := ↥K') (g.toSubring K'.toSubring ⋯)

Tactic:
rw [natDegree_toSubring, natDegree_map]

Premises used: Polynomial.natDegree_toSubring, Polynomial.natDegree_map
-- 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
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
⊢ Module.Finite.{u_1, u_2} F ↥⊥

Tactic:
Subalgebra.finite_bot

Premises used: Set.Mem, Subsemiring.copy, AlgHom.range, RingHom.rangeS, Subalgebra.finite_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
inst_3 : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
⊢ ∃ (L : IntermediateField F E), FiniteDimensional.{u_1, u_2} F ↥L ∧ 0 < finrank.{u_1, u_2} F ↥L

Tactic:
⟨⊥, Subalgebra.finite_bot, finrank_pos⟩

Premises used: Bot.bot, And.intro, Exists.intro, Module.finrank_pos, Subalgebra.finite_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
inst_3 : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
⊢ ∃ (L : IntermediateField F E), FiniteDimensional.{u_1, u_2} F ↥L ∧ 0 < finrank.{u_1, u_2} F ↥L

Tactic:
exact ⟨⊥, Subalgebra.finite_bot, 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 : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
n : ℕ
ih : ∃ (L : IntermediateField F E), FiniteDimensional.{u_1, u_2} F ↥L ∧ n < finrank.{u_1, u_2} F ↥L
succ :
  ∀ (L : IntermediateField F E) (fin : FiniteDimensional.{u_1, u_2} F ↥L) (hn : 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 + 1 < finrank.{u_1, u_2} F ↥L

Tactic:
obtain ⟨L, fin, hn⟩ := ih
-- 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 : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥L
hn : n < finrank.{u_1, u_2} F ↥L
contrapose! : ∀ (hnfd : ∀ (x : E), x ∈ L), FiniteDimensional F E
⊢ ∃ (x : E), x ∉ L

Tactic:
contrapose! hnfd
-- 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
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥L
hn : n < finrank.{u_1, u_2} F ↥L
hnfd : ∀ (x : E), x ∈ L
⊢ FiniteDimensional.{u_1, u_2} F ↥⊤

Tactic:
rw [show L = ⊤ from eq_top_iff.2 fun x _ ↦ hnfd x] at fin

Premises used: Iff.mpr, eq_top_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
inst_3 : Algebra.IsAlgebraic F E
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥L
hn : n < finrank.{u_1, u_2} F ↥L
hnfd : ∀ (x : E), x ∈ L
fin₁ : FiniteDimensional.{u_1, u_2} F ↥⊤
⊢ n < finrank.{u_1, u_2} F ↥L

Tactic:
rw [show L = ⊤ from eq_top_iff.2 fun x _ ↦ hnfd x] at fin

Premises used: Iff.mpr, eq_top_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
inst_3 : Algebra.IsAlgebraic F E
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥L
hn : n < finrank.{u_1, u_2} F ↥L
hnfd : ∀ (x : E), x ∈ L
fin₁ : FiniteDimensional.{u_1, u_2} F ↥⊤
hn₁ : n < finrank.{u_1, u_2} F ↥L
⊢ ∀ (x : E), x ∈ L

Tactic:
rw [show L = ⊤ from eq_top_iff.2 fun x _ ↦ hnfd x] at fin

Premises used: Iff.mpr, eq_top_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
inst_3 : Algebra.IsAlgebraic F E
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥⊤
hn : n < finrank.{u_1, u_2} F ↥L
hnfd : ∀ (x : E), x ∈ L
⊢ FiniteDimensional F E

Tactic:
topEquiv.toLinearEquiv.finiteDimensional

Premises used: LinearEquiv.finiteDimensional
-- 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
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥⊤
hn : n < finrank.{u_1, u_2} F ↥L
hnfd : ∀ (x : E), x ∈ L
⊢ FiniteDimensional F E

Tactic:
exact topEquiv.toLinearEquiv.finiteDimensional

Premises used: LinearEquiv.finiteDimensional
-- 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 : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥L
hn : n < finrank.{u_1, u_2} F ↥L
succ :
  ∀ (x : E) (hx : x ∉ 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 + 1 < finrank.{u_1, u_2} F ↥L

Tactic:
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
-- 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 : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥L
hn : n < finrank.{u_1, u_2} F ↥L
x : E
hx : x ∉ L
L' : IntermediateField F E := L ⊔ F⟮x⟯
⊢ FiniteDimensional.{u_1, u_2} F ↥F⟮x⟯

Tactic:
haveI := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (R := F) x)
-- 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 : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥L
hn : n < finrank.{u_1, u_2} F ↥L
x : E
hx : x ∉ L
L' : IntermediateField F E := L ⊔ F⟮x⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮x⟯
⊢ ∃ (L : IntermediateField F E), FiniteDimensional.{u_1, u_2} F ↥L ∧ n + 1 < finrank.{u_1, u_2} F ↥L

Tactic:
⟨L', inferInstance, by_contra fun h ↦ ?_⟩

Premises used: inferInstance, And.intro, Exists.intro, by_contra
-- 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 : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥L
hn : n < finrank.{u_1, u_2} F ↥L
x : E
hx : x ∉ L
L' : IntermediateField F E := L ⊔ F⟮x⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮x⟯
succ : ∀ (h : ¬n + 1 < finrank.{u_1, u_2} F ↥L'), False
⊢ ∃ (L : IntermediateField F E), FiniteDimensional.{u_1, u_2} F ↥L ∧ n + 1 < finrank.{u_1, u_2} F ↥L

Tactic:
refine ⟨L', inferInstance, by_contra fun 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
inst_3 : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥L
hn : n < finrank.{u_1, u_2} F ↥L
x : E
hx : x ∉ L
L' : IntermediateField F E := L ⊔ F⟮x⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮x⟯
h : ¬n + 1 < finrank.{u_1, u_2} F ↥L'
⊢ L = L'

Tactic:
have h1 : L = L' := eq_of_le_of_finrank_le le_sup_left ((not_lt.1 h).trans hn)
-- 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 : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥L
hn : n < finrank.{u_1, u_2} F ↥L
x : E
hx : x ∉ L
L' : IntermediateField F E := L ⊔ F⟮x⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮x⟯
h : ¬n + 1 < finrank.{u_1, u_2} F ↥L'
h1 : L = L'
⊢ F⟮x⟯ ≤ L'

Tactic:
have h2 : F⟮x⟯ ≤ L' := le_sup_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
inst_3 : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥L
hn : n < finrank.{u_1, u_2} F ↥L
x : E
hx : x ∉ L
L' : IntermediateField F E := L ⊔ F⟮x⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮x⟯
h : ¬n + 1 < finrank.{u_1, u_2} F ↥L'
h1 : L = L'
h2 : F⟮x⟯ ≤ L'
⊢ False

Tactic:
hx <| (h1.symm ▸ h2) <| mem_adjoin_simple_self F x
-- 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 : ℕ
L : IntermediateField F E
fin : FiniteDimensional.{u_1, u_2} F ↥L
hn : n < finrank.{u_1, u_2} F ↥L
x : E
hx : x ∉ L
L' : IntermediateField F E := L ⊔ F⟮x⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮x⟯
h : ¬n + 1 < finrank.{u_1, u_2} F ↥L'
h1 : L = L'
h2 : F⟮x⟯ ≤ L'
⊢ False

Tactic:
exact hx <| (h1.symm ▸ h2) <| mem_adjoin_simple_self F x

Premises used: IntermediateField.mem_adjoin_simple_self