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

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

Tactic:
let f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯

Result:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯

Proof state:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Tactic:
have αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯ := mem_adjoin_simple_self F _

Result:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Proof state:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + y • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Tactic:
simp only [← heq] at αyβ_in_K

Result:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Proof state:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : α + x • β - (α + y • β) ∈ F⟮α + x • β⟯
⊢ α + x • β - (α + y • β) = x • β - y • β

Tactic:
abel1

Result:
no goals

Proof state:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : β ∈ F⟮α + x • β⟯
α_in_K : α ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Tactic:
rintro x (rfl | rfl) <;> assumption

Result:
no goals

Proof state:
case intro.intro.intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯

Tactic:
use α + x • β

Result:
case h
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α, β⟯ = F⟮α + x • β⟯

Proof state:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
α_in_Fαβ : α ∈ F⟮α, β⟯
β_in_Fαβ : β ∈ F⟮α, β⟯
⊢ α + x • β ∈ F⟮α, β⟯

Tactic:
exact F⟮α, β⟯.add_mem α_in_Fαβ (F⟮α, β⟯.smul_mem β_in_Fαβ)

Result:
no goals

Proof state:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Tactic:
have αyβ_in_K : α + y • β ∈ F⟮α + y • β⟯ := mem_adjoin_simple_self F _

Result:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + y • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Proof state:
case h
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α, β⟯ = F⟮α + x • β⟯

Tactic:
apply le_antisymm

Result:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α, β⟯ ≤ F⟮α + x • β⟯

case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α + x • β⟯ ≤ F⟮α, β⟯

Proof state:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
α_in_Fαβ : α ∈ F⟮α, β⟯
⊢ α + x • β ∈ F⟮α, β⟯

Tactic:
have β_in_Fαβ : β ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert_of_mem α rfl)

Result:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
α_in_Fαβ : α ∈ F⟮α, β⟯
β_in_Fαβ : β ∈ F⟮α, β⟯
⊢ α + x • β ∈ F⟮α, β⟯

Proof state:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : β ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Tactic:
have α_in_K : α ∈ F⟮α + x • β⟯ := by
  convert ← sub_mem αxβ_in_K (smul_mem _ β_in_K)
  apply add_sub_cancel_right

Result:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x => F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : β ∈ F⟮α + x • β⟯
α_in_K : α ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯