-- Mathlib/FieldTheory/PrimitiveElement.lean
theorem exists_primitive_element_of_finite_intermediateField
    [Finite (IntermediateField F E)] (K : IntermediateField F E) : ∃ α : E, F⟮α⟯ = K

Proof state:
case inr.ih.intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
β α : E
⊢ ∃ α_1, F⟮α_1⟯ = restrictScalars F (↥F⟮α⟯)⟮β⟯

Tactic:
simp_rw [adjoin_simple_adjoin_simple, eq_comm]

Result:
case inr.ih.intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
β α : E
⊢ ∃ α_1, F⟮α, β⟯ = F⟮α_1⟯

Proof state:
case inl
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Finite F
⊢ ∃ α, F⟮α⟯ = K

Tactic:
obtain ⟨α, h⟩ := exists_primitive_element_of_finite_bot F K

Result:
case inl.intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Finite F
α : ↥K
h : F⟮α⟯ = ⊤
⊢ ∃ α, F⟮α⟯ = K

Proof state:
case inr
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
⊢ ∃ α, F⟮α⟯ = K

Tactic:
apply induction_on_adjoin (fun K ↦ ∃ α : E, F⟮α⟯ = K) ⟨0, adjoin_zero⟩

Result:
case inr.ih
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
⊢ ∀ (K : IntermediateField F E) (x : E), (∃ α, F⟮α⟯ = K) → ∃ α, F⟮α⟯ = restrictScalars F (↥K)⟮x⟯

Proof state:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
⊢ ∃ α, F⟮α⟯ = K

Tactic:
rcases finite_or_infinite F with (_ | _)

Result:
case inl
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Finite F
⊢ ∃ α, F⟮α⟯ = K

case inr
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
⊢ ∃ α, F⟮α⟯ = K

Proof state:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Finite F
α : ↥K
h : F⟮α⟯ = ⊤
⊢ F⟮↑α⟯ = K

Tactic:
simpa only [lift_adjoin_simple, lift_top] using congr_arg lift h

Result:
no goals

Proof state:
case inl.intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Finite F
α : ↥K
h : F⟮α⟯ = ⊤
⊢ ∃ α, F⟮α⟯ = K

Tactic:
exact ⟨α, by simpa only [lift_adjoin_simple, lift_top] using congr_arg lift h⟩

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
⊢ ∃ α, F⟮α⟯ = K

Tactic:
haveI := FiniteDimensional.of_finite_intermediateField F E

Result:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
⊢ ∃ α, F⟮α⟯ = K

Proof state:
case inr.ih
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
⊢ ∀ (K : IntermediateField F E) (x : E), (∃ α, F⟮α⟯ = K) → ∃ α, F⟮α⟯ = restrictScalars F (↥K)⟮x⟯

Tactic:
rintro K β ⟨α, rfl⟩

Result:
case inr.ih.intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
β α : E
⊢ ∃ α_1, F⟮α_1⟯ = restrictScalars F (↥F⟮α⟯)⟮β⟯

Proof state:
case inr.ih.intro
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
β α : E
⊢ ∃ α_1, F⟮α, β⟯ = F⟮α_1⟯

Tactic:
exact primitive_element_inf_aux_of_finite_intermediateField F α β

Result:
no goals