awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
t : Finset E
⊢ FG (adjoin F (↑t : Set E))

Tactic:
⟨t, rfl⟩

Premises used: IntermediateField.FG, Exists.intro, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : IntermediateField F E
⊢ S.FG ↔ ∃ (t : Set E), t.Finite ∧ adjoin F t = S

Tactic:
Iff.symm Set.exists_finite_iff_finset

Premises used: Set.exists_finite_iff_finset, Iff.symm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
t : Set E
h : t.Finite
⊢ FG (adjoin F t)

Tactic:
fg_def.mpr ⟨t, h, rfl⟩

Premises used: Iff.mpr, IntermediateField.fg_def, And.intro, Exists.intro, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq (α := IntermediateField F E) (adjoin F (↑∅ : Set E)) ⊥

Tactic:
simp only [Finset.coe_empty, adjoin_empty]

Premises used: Finset.coe_empty, IntermediateField.adjoin_empty
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : IntermediateField F E
hS : S.FG
hT : T.FG
obtain : ∀ (s : Finset E), (adjoin F (↑s : Set E) ⊔ T).FG
⊢ (S ⊔ T).FG

Tactic:
obtain ⟨s, rfl⟩ := hS

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
T : IntermediateField F E
hT : T.FG
s : Finset E
obtain : ∀ (t : Finset E), FG (adjoin F (↑s : Set E) ⊔ adjoin F (↑t : Set E))
⊢ (adjoin F (↑s : Set E) ⊔ T).FG

Tactic:
obtain ⟨t, rfl⟩ := hT

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
s t : Finset E
rw : FG (adjoin F (↑(s ∪ t) : Set E))
⊢ FG (adjoin F (↑s : Set E) ⊔ adjoin F (↑t : Set E))

Tactic:
rw [← adjoin_union, ← Finset.coe_union]

Premises used: IntermediateField.adjoin_union, Finset.coe_union
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
s t : Finset E
classical : FG (adjoin F (↑(s ∪ t) : Set E))
⊢ FG (adjoin F (↑s : Set E) ⊔ adjoin F (↑t : Set E))

Tactic:
classical rw [← adjoin_union, ← Finset.coe_union]

Premises used: IntermediateField.adjoin_union, Finset.coe_union
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
s t : Finset E
⊢ FG (adjoin F (↑(s ∪ t) : Set E))

Tactic:
fg_adjoin_finset _

Premises used: IntermediateField.fg_adjoin_finset
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
s t : Finset E
⊢ FG (adjoin F (↑(s ∪ t) : Set E))

Tactic:
exact fg_adjoin_finset _

Premises used: IntermediateField.fg_adjoin_finset
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Sort u_3
inst_3 : Finite ι
S : ι → IntermediateField F E
h : ∀ (i : ι), (S i).FG
choose :
  ∀ (s : (i : ι) → Finset E) (hs : ∀ (i : ι), adjoin F (↑(s i) : Set E) = S i),
    FG.{u_1, u_2} (F := F) (E := E) (⨆ (i : ι), S i)
⊢ FG.{u_1, u_2} (F := F) (E := E) (⨆ (i : ι), S i)

Tactic:
choose s hs using h
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Sort u_3
inst_3 : Finite ι
S : ι → IntermediateField F E
s : (i : ι) → Finset E
hs : ∀ (i : ι), adjoin F (↑(s i) : Set E) = S i
simp_rw : FG.{u_1, u_2} (E := E) (adjoin F (⋃ (i : ι), (↑(s i) : Set E)))
⊢ FG.{u_1, u_2} (F := F) (E := E) (⨆ (i : ι), S i)

Tactic:
simp_rw [← hs, ← adjoin_iUnion]

Premises used: IntermediateField.adjoin_iUnion
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Sort u_3
inst_3 : Finite ι
S : ι → IntermediateField F E
s : (i : ι) → Finset E
hs : ∀ (i : ι), adjoin F (↑(s i) : Set E) = S i
⊢ FG.{u_1, u_2} (E := E) (adjoin F (⋃ (i : ι), (↑(s i) : Set E)))

Tactic:
fg_adjoin_of_finite (Set.finite_iUnion fun _ ↦ Finset.finite_toSet _)

Premises used: Set.finite_iUnion, IntermediateField.fg_adjoin_of_finite, Finset.finite_toSet
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Sort u_3
inst_3 : Finite ι
S : ι → IntermediateField F E
s : (i : ι) → Finset E
hs : ∀ (i : ι), adjoin F (↑(s i) : Set E) = S i
⊢ FG.{u_1, u_2} (E := E) (adjoin F (⋃ (i : ι), (↑(s i) : Set E)))

Tactic:
exact fg_adjoin_of_finite (Set.finite_iUnion fun _ ↦ Finset.finite_toSet _)

Premises used: Set.finite_iUnion, IntermediateField.fg_adjoin_of_finite, Finset.finite_toSet
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
⊢ P (adjoin F (↑S : Set E))

Tactic:
Finset.induction_on' S ?_ (fun _ _ ha _ _ h => ?_)

Premises used: Finset.induction_on'
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
refine_1 : P (adjoin F (↑∅ : Set E))
refine_2 :
  ∀ (x : E) (x_1 : Finset E) (ha : x ∈ S),
    x_1 ⊆ S → x ∉ x_1 → ∀ (h : P (adjoin F (↑x_1 : Set E))), P (adjoin F (↑(insert x x_1) : Set E))
⊢ P (adjoin F (↑S : Set E))

Tactic:
refine Finset.induction_on' S ?_ (fun _ _ ha _ _ h => ?_)
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
⊢ P (adjoin F (↑∅ : Set E))

Tactic:
simp [base]
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
x : E
x_1 : Finset E
ha : x ∈ S
h_1 : x_1 ⊆ S
h_2 : x ∉ x_1
h : P (adjoin F (↑x_1 : Set E))
refine_2 : P (restrictScalars F (L' := ↥(adjoin F (↑x_1 : Set E))) (↥(adjoin F (↑x_1 : Set E)))⟮x⟯)
⊢ P (adjoin F (↑(insert x x_1) : Set E))

Tactic:
rw [Finset.coe_insert, Set.insert_eq, Set.union_comm, ← adjoin_adjoin_left]

Premises used: Set.insert_eq, Set.union_comm, IntermediateField.adjoin_adjoin_left, Finset.coe_insert
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
x : E
x_1 : Finset E
ha : x ∈ S
h_1 : x_1 ⊆ S
h_2 : x ∉ x_1
h : P (adjoin F (↑x_1 : Set E))
⊢ P (restrictScalars F (L' := ↥(adjoin F (↑x_1 : Set E))) (↥(adjoin F (↑x_1 : Set E)))⟮x⟯)

Tactic:
ih (adjoin F _) _ ha h

Premises used: IntermediateField.adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
x : E
x_1 : Finset E
ha : x ∈ S
h_1 : x_1 ⊆ S
h_2 : x ∉ x_1
h : P (adjoin F (↑x_1 : Set E))
⊢ P (restrictScalars F (L' := ↥(adjoin F (↑x_1 : Set E))) (↥(adjoin F (↑x_1 : Set E)))⟮x⟯)

Tactic:
exact ih (adjoin F _) _ ha h

Premises used: IntermediateField.adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
refine_1 : P (adjoin F (↑∅ : Set E))
refine_2 refine_2₁ :
  ∀ (x : E) (x_1 : Finset E) (ha : x ∈ S),
    x_1 ⊆ S → x ∉ x_1 → ∀ (h : P (adjoin F (↑x_1 : Set E))), P (adjoin F (↑(insert x x_1) : Set E))
⊢ P (adjoin F (↑S : Set E))

Tactic:
classical
  refine Finset.induction_on' S ?_ (fun _ _ ha _ _ h => ?_)
  · simp [base]
  · rw [Finset.coe_insert, Set.insert_eq, Set.union_comm, ← adjoin_adjoin_left]
    exact ih (adjoin F _) _ ha h

Premises used: Set.insert_eq, Set.union_comm, IntermediateField.adjoin_adjoin_left, Finset.coe_insert
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
K : IntermediateField F E
hK : K.FG
obtain : ∀ (S : Finset E), P (adjoin F (↑S : Set E))
⊢ P K

Tactic:
obtain ⟨S, rfl⟩ := hK

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
S : Finset E
⊢ P (adjoin F (↑S : Set E))

Tactic:
induction_on_adjoin_finset S P base fun K x _ hK => ih K x hK

Premises used: IntermediateField.induction_on_adjoin_finset
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
S : Finset E
⊢ P (adjoin F (↑S : Set E))

Tactic:
exact induction_on_adjoin_finset S P base fun K x _ hK => ih K x hK

Premises used: IntermediateField.induction_on_adjoin_finset
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
S : IntermediateField K L'
⊢ map f (comap f S) = S ⊓ f.fieldRange

Tactic:
SetLike.coe_injective Set.image_preimage_eq_inter_range

Premises used: SetLike.coe_injective, Set.image_preimage_eq_inter_range
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
S : IntermediateField K L'
h : S ≤ f.fieldRange
⊢ map f (comap f S) = S

Tactic:
simpa only [inf_of_le_left h] using map_comap_eq f S

Premises used: inf_of_le_left, IntermediateField.map_comap_eq
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := L) (β := L') (⇑f : (a : L) → L')
S : IntermediateField K L'
⊢ map f (comap f S) = S

Tactic:
SetLike.coe_injective (Set.image_preimage_eq _ hf)

Premises used: Set.image_preimage_eq, SetLike.coe_injective
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
f : L →ₐ[K] L'
S : IntermediateField K L
⊢ comap f (map f S) = S

Tactic:
SetLike.coe_injective (Set.preimage_image_eq _ f.injective)

Premises used: SetLike.coe_injective, RingHom.injective, AlgHom.toRingHom, Set.preimage_image_eq
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
L : Type u_2
inst : Field L
F : Subfield L
h : ∀ (x : L), x ∈ extendScalars ⋯ ↔ Membership.mem (γ := IntermediateField (↥F) L) ⊥ x
⊢ extendScalars ⋯ = ⊥

Tactic:
ext x
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
L : Type u_2
inst : Field L
F : Subfield L
x : L
h : x ∈ F ↔ Membership.mem (γ := Set L) (Set.range (ι := ↥F) (⇑(algebraMap (↥F) L) : (a : ↥F) → L)) x
⊢ x ∈ extendScalars ⋯ ↔ Membership.mem (γ := IntermediateField (↥F) L) ⊥ x

Tactic:
rw [mem_extendScalars, IntermediateField.mem_bot]

Premises used: Subfield.mem_extendScalars, IntermediateField.mem_bot
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
L : Type u_2
inst : Field L
F : Subfield L
x : L
⊢ x ∈ F ↔ Membership.mem (γ := Set L) (Set.range (ι := ↥F) (⇑(algebraMap (↥F) L) : (a : ↥F) → L)) x

Tactic:
⟨fun h ↦ ⟨⟨x, h⟩, rfl⟩, ?_⟩

Premises used: Subtype.mk, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
L : Type u_2
inst : Field L
F : Subfield L
x : L
h : Membership.mem (γ := Set L) (Set.range (ι := ↥F) (⇑(algebraMap (↥F) L) : (a : ↥F) → L)) x → x ∈ F
⊢ x ∈ F ↔ Membership.mem (γ := Set L) (Set.range (ι := ↥F) (⇑(algebraMap (↥F) L) : (a : ↥F) → L)) x

Tactic:
refine ⟨fun h ↦ ⟨⟨x, h⟩, rfl⟩, ?_⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
L : Type u_2
inst : Field L
F : Subfield L
y : ↥F
⊢ Membership.mem (α := L) F ((algebraMap (↥F) L : (a : ↥F) → L) y : L)

Tactic:
y.2

Premises used: Set.Mem, Subtype.property
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
L : Type u_2
inst : Field L
F : Subfield L
y : ↥F
⊢ Membership.mem (α := L) F ((algebraMap (↥F) L : (a : ↥F) → L) y : L)

Tactic:
exact y.2

Premises used: Subtype.property
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
L : Type u_2
inst : Field L
F : Subfield L
⊢ Eq.{u_2 + 1} (α := Subfield L) (IntermediateField.toSubfield (K := ↥F) (extendScalars (E := ⊤) ⋯))
    (IntermediateField.toSubfield (K := ↥F) ⊤)

Tactic:
simp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
L : Type u_2
inst : Field L
F E E' : Subfield L
h : F ≤ E
h' : F ≤ E'
⊢ extendScalars h ⊔ extendScalars h' = extendScalars (E := E ⊔ E') ⋯

Tactic:
((extendScalars.orderIso F).map_sup ⟨_, h⟩ ⟨_, h'⟩).symm

Premises used: Subfield.extendScalars.orderIso, Set.Mem, setOf, Subtype.mk, OrderIso.map_sup, Subfield.extendScalars, Subfield.toIntermediateField, Eq.symm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
L : Type u_2
inst : Field L
F E E' : Subfield L
h : F ≤ E
h' : F ≤ E'
⊢ extendScalars h ⊓ extendScalars h' = extendScalars ⋯

Tactic:
((extendScalars.orderIso F).map_inf ⟨_, h⟩ ⟨_, h'⟩).symm

Premises used: Subfield.extendScalars.orderIso, OrderIso.map_inf, Subtype.mk, Subfield.extendScalars, Subfield.toIntermediateField, Eq.symm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
K : Type u_1
inst : Field K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
⊢ Eq (α := IntermediateField K L) (restrictScalars K (extendScalars ⋯)) (restrictScalars K (L' := ↥F) ⊥)

Tactic:
simp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
K : Type u_1
inst : Field K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
⊢ Eq.{u_2 + 1} (α := IntermediateField K L) (restrictScalars K (L' := ↥F) (extendScalars (E := ⊤) ⋯))
    (restrictScalars K (L' := ↥F) ⊤)

Tactic:
simp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
K : Type u_1
inst : Field K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
F E E' : IntermediateField K L
h : F ≤ E
h' : F ≤ E'
⊢ extendScalars h ⊔ extendScalars h' = extendScalars (E := E ⊔ E') ⋯

Tactic:
((extendScalars.orderIso F).map_sup ⟨_, h⟩ ⟨_, h'⟩).symm

Premises used: Set.Mem, setOf, IntermediateField.extendScalars, Subtype.mk, IntermediateField.extendScalars.orderIso, OrderIso.map_sup, Subfield.extendScalars, Subfield.toIntermediateField, Eq.symm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
K : Type u_1
inst : Field K
L : Type u_2
inst_1 : Field L
inst_2 : Algebra K L
F E E' : IntermediateField K L
h : F ≤ E
h' : F ≤ E'
⊢ extendScalars h ⊓ extendScalars h' = extendScalars ⋯

Tactic:
((extendScalars.orderIso F).map_inf ⟨_, h⟩ ⟨_, h'⟩).symm

Premises used: OrderIso.map_inf, IntermediateField.extendScalars, Subtype.mk, IntermediateField.extendScalars.orderIso, Subfield.extendScalars, Subfield.toIntermediateField, Eq.symm
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
R : Type u_3
inst_3 : CommRing R
inst_4 : Algebra R K
inst_5 : Algebra R L
inst_6 : IsScalarTower R K L
x : ↥S
⊢ IsIntegral R (↑x : L) ↔ IsIntegral R x

Tactic:
isIntegral_algHom_iff (S.val.restrictScalars R) Subtype.val_injective

Premises used: Subtype.val_injective, isIntegral_algHom_iff, AlgHom.restrictScalars, IntermediateField.val
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
inst_3 : Algebra.IsAlgebraic K L
⊢ Algebra.IsAlgebraic.{u_1, u_2} K ↥S

Tactic:
Algebra.IsAlgebraic.of_injective S.val S.val.injective

Premises used: RingHom.injective, AlgHom.toRingHom, IntermediateField.val, Algebra.IsAlgebraic.of_injective
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
inst_3 : Algebra.IsAlgebraic K L
⊢ Algebra.IsAlgebraic (↥S) L

Tactic:
Algebra.IsAlgebraic.tower_top (K := K) S

Premises used: Algebra.IsAlgebraic.tower_top, Membership.mem, Subtype
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S F E : IntermediateField K L
inst_3 : FiniteDimensional K L
⊢ FiniteDimensional.{u_1, u_2} K ↥F

Tactic:
.left K F L

Premises used: Membership.mem, Subtype, FiniteDimensional.left
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S F E : IntermediateField K L
inst_3 : FiniteDimensional K L
⊢ FiniteDimensional (↥F) L

Tactic:
.right K F L

Premises used: Membership.mem, Subtype, FiniteDimensional.right
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
⊢ Module.rank K ↥F.toSubalgebra = Module.rank K ↥F

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
⊢ finrank.{u_1, u_2} K ↥F.toSubalgebra = finrank.{u_1, u_2} K ↥F

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
hfin : FiniteDimensional.{u_1, u_2} K ↥E
h_le : F ≤ E
h_finrank : finrank.{u_1, u_2} K ↥E ≤ finrank.{u_1, u_2} K ↥F
⊢ F = E

Tactic:
haveI : Module.Finite K E.toSubalgebra := hfin
  toSubalgebra_injective <| Subalgebra.eq_of_le_of_finrank_le h_le h_finrank

Premises used: Subalgebra.eq_of_le_of_finrank_le, IntermediateField.toSubalgebra_injective
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional.{u_1, u_2} K ↥E
h_le : F ≤ E
h_finrank : finrank.{u_1, u_2} K ↥F = finrank.{u_1, u_2} K ↥E
⊢ F = E

Tactic:
eq_of_le_of_finrank_le h_le h_finrank.ge

Premises used: Eq.ge, IntermediateField.eq_of_le_of_finrank_le
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
apply : finrank.{u_1, u_2} K ↥E ≤ finrank.{u_1, u_2} K ↥F
⊢ F = E

Tactic:
apply eq_of_le_of_finrank_le h_le

Premises used: IntermediateField.eq_of_le_of_finrank_le
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
⊢ finrank.{u_1, u_2} K ↥F * finrank (↥F) L = finrank K L

Tactic:
have h1 := finrank_mul_finrank K F L
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
h1 : finrank.{u_1, u_2} K ↥F * finrank (↥F) L = finrank K L
⊢ finrank.{u_1, u_2} K ↥E * finrank (↥E) L = finrank K L

Tactic:
have h2 := finrank_mul_finrank K E L
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
h1 : finrank.{u_1, u_2} K ↥F * finrank (↥F) L = finrank K L
h2 : finrank.{u_1, u_2} K ↥E * finrank (↥E) L = finrank K L
⊢ 0 < finrank (↥E) L

Tactic:
have h3 : 0 < finrank E L := finrank_pos
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional K L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
h1 : finrank.{u_1, u_2} K ↥F * finrank (↥F) L = finrank K L
h2 : finrank.{u_1, u_2} K ↥E * finrank (↥E) L = finrank K L
h3 : 0 < finrank (↥E) L
nlinarith :
  finrank.{u_1, u_2} K ↥F < finrank.{u_1, u_2} K ↥E →
    -1 + -(HMul.hMul (α := ℤ) (↑(finrank.{u_1, u_2} K ↥F) : ℤ) (↑(finrank (↥F) L) : ℤ) - (↑(finrank K L) : ℤ)) +
              (HMul.hMul (α := ℤ) (↑(finrank.{u_1, u_2} K ↥E) : ℤ) (↑(finrank (↥E) L) : ℤ) - (↑(finrank K L) : ℤ)) +
            (HAdd.hAdd (α := ℤ) 0 1 - (↑(finrank (↥E) L) : ℤ)) +
          (0 -
            HSub.hSub (α := ℤ) 0 (↑(finrank (↥E) L) : ℤ) *
              (HAdd.hAdd (α := ℤ) (↑(finrank.{u_1, u_2} K ↥F) : ℤ) 1 - (↑(finrank.{u_1, u_2} K ↥E) : ℤ))) +
        (0 -
          HSub.hSub (α := ℤ) 0 (↑(finrank.{u_1, u_2} K ↥F) : ℤ) *
            HSub.hSub (α := ℤ) (↑(finrank (↥F) L) : ℤ) (↑(finrank (↥E) L) : ℤ)) =
      0
⊢ finrank.{u_1, u_2} K ↥E ≤ finrank.{u_1, u_2} K ↥F

Tactic:
nlinarith
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
⊢ F = E

Tactic:
le_antisymm h_le (fun l hl ↦ ?_)

Premises used: le_antisymm
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
refine : ∀ (l : L) (hl : l ∈ E), l ∈ F
⊢ F = E

Tactic:
refine le_antisymm h_le (fun l hl ↦ ?_)

Premises used: le_antisymm