awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x
h : FiniteDimensional Ft K
b : Module.Basis (Fin (Module.finrank Ft K)) Ft K := Module.finBasis Ft K
c : Ft
x : K
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := F⟮X⟯) ((e.symm : (a : Ft) → F⟮X⟯) c : F⟮X⟯) x =
    HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) ((e.symm : (a : Ft) → F⟮X⟯) c : F⟮X⟯) : Ft) x

Tactic:
(this (e.symm c) x).symm

Premises used: AlgEquiv.symm, Eq.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x
h : FiniteDimensional Ft K
b : Module.Basis (Fin (Module.finrank Ft K)) Ft K := Module.finBasis Ft K
c : Ft
x : K
h₁ : c = (e : (a : F⟮X⟯) → Ft) ((e.symm : (a : Ft) → F⟮X⟯) c : F⟮X⟯)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := F⟮X⟯) ((e.symm.toRingEquiv : (a : Ft) → F⟮X⟯) c : F⟮X⟯) x = c • x

Tactic:
convert! (this (e.symm c) x).symm

Premises used: AlgEquiv.symm, Eq.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
Ft : Type u_3
inst_2 : Field Ft
inst_3 : Algebra.{u_1, u_3} F[X] Ft
inst_4 : IsFractionRing.{u_1, u_3} F[X] Ft
inst_5 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_6 : Algebra Ft K
inst_7 : Algebra.{u_1, u_2} F[X] K
inst_8 : IsScalarTower.{u_1, u_3, u_2} F[X] Ft K
inst_9 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
e : AlgEquiv.{u_1, u_1, u_3} F[X] F⟮X⟯ Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), HSMul.hSMul.{u_3, u_2, u_2} (α := Ft) ((e : (a : F⟮X⟯) → Ft) c : Ft) x = c • x
h : FiniteDimensional Ft K
b : Module.Basis (Fin (Module.finrank Ft K)) Ft K := Module.finBasis Ft K
c : Ft
x : K
⊢ c = (e : (a : F⟮X⟯) → Ft) ((e.symm : (a : Ft) → F⟮X⟯) c : F⟮X⟯)

Tactic:
simp only [e.apply_symm_apply]

Premises used: AlgEquiv.apply_symm_apply
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
rw :
  Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := K)
    (⇑(@RingHom.comp _ F⟮X⟯ _ _ Semiring.toNonAssocSemiring _ (algebraMap F⟮X⟯ K) (algebraMap F[X] F⟮X⟯)) :
      (a : F[X]) → K)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := K) (⇑(algebraMap F[X] K) : (a : F[X]) → K)

Tactic:
rw [IsScalarTower.algebraMap_eq F[X] F⟮X⟯ K]

Premises used: Polynomial, RatFunc, IsScalarTower.algebraMap_eq
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := K)
    (⇑(@RingHom.comp _ F⟮X⟯ _ _ Semiring.toNonAssocSemiring _ (algebraMap F⟮X⟯ K) (algebraMap F[X] F⟮X⟯)) :
      (a : F[X]) → K)

Tactic:
(algebraMap F⟮X⟯ K).injective.comp (IsFractionRing.injective F[X] F⟮X⟯)

Premises used: Algebra.algebraMap, IsFractionRing.injective, RingHom.injective, Polynomial, RatFunc, Function.Injective.comp
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := K)
    (⇑(@RingHom.comp _ F⟮X⟯ _ _ Semiring.toNonAssocSemiring _ (algebraMap F⟮X⟯ K) (algebraMap F[X] F⟮X⟯)) :
      (a : F[X]) → K)

Tactic:
exact (algebraMap F⟮X⟯ K).injective.comp (IsFractionRing.injective F[X] F⟮X⟯)

Premises used: Algebra.algebraMap, IsFractionRing.injective, RingHom.injective, Polynomial, RatFunc, Function.Injective.comp
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
⊢ IsDomain.{u_2} ↥(ringOfIntegers F K)

Tactic:
(ringOfIntegers F K).isDomain

Premises used: Set.Mem, Subalgebra.isDomain, FunctionField.ringOfIntegers
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
⊢ IsIntegralClosure.{u_2, u_1, u_2} (↥(ringOfIntegers F K)) F[X] K

Tactic:
integralClosure.isIntegralClosure _ _

Premises used: Set.Mem, integralClosure.isIntegralClosure, FunctionField.ringOfIntegers
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := K) (⇑(algebraMap F[X] K) : (a : F[X]) → K)

Tactic:
have hinj : Function.Injective (algebraMap F[X] K) := by
    rw [IsScalarTower.algebraMap_eq F[X] F⟮X⟯ K]
    exact (algebraMap F⟮X⟯ K).injective.comp (IsFractionRing.injective F[X] F⟮X⟯)
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := K) (⇑(algebraMap F[X] K) : (a : F[X]) → K)
rw :
  ∀ (a : F[X]),
    Eq.{u_2 + 1} (α := ↥(ringOfIntegers F K))
        ((algebraMap F[X] ↥(ringOfIntegers F K) : (a : F[X]) → ↥(ringOfIntegers F K)) a : ↥(ringOfIntegers F K))
        (0 : ↥(ringOfIntegers F K)) →
      a = 0
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := ↥(ringOfIntegers F K))
    (⇑(algebraMap F[X] ↥(ringOfIntegers F K)) : (a : F[X]) → ↥(ringOfIntegers F K))

Tactic:
rw [injective_iff_map_eq_zero (algebraMap F[X] (↥(ringOfIntegers F K)))]

Premises used: Algebra.algebraMap, Membership.mem, Subtype, Polynomial, injective_iff_map_eq_zero, FunctionField.ringOfIntegers
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := K) (⇑(algebraMap F[X] K) : (a : F[X]) → K)
p : F[X]
hp :
  Eq.{u_2 + 1} (α := ↥(ringOfIntegers F K))
    ((algebraMap F[X] ↥(ringOfIntegers F K) : (a : F[X]) → ↥(ringOfIntegers F K)) p : ↥(ringOfIntegers F K))
    (0 : ↥(ringOfIntegers F K))
⊢ Eq.{u_2 + 1} (α := K) (↑((algebraMap F[X] ↥(ringOfIntegers F K) : (a : F[X]) → ↥(ringOfIntegers F K)) p) : K) 0

Tactic:
rw [← Subtype.coe_inj, Subalgebra.coe_zero] at hp

Premises used: Subtype.coe_inj, Subalgebra.coe_zero
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := F[X]) (β := K) (⇑(algebraMap F[X] K) : (a : F[X]) → K)
p : F[X]
hp : Eq.{u_2 + 1} (α := K) (↑((algebraMap F[X] ↥(ringOfIntegers F K) : (a : F[X]) → ↥(ringOfIntegers F K)) p) : K) 0
rw :
  ∀ (hinj : ∀ (a : F[X]), Eq.{u_2 + 1} (α := K) ((algebraMap F[X] K : (a : F[X]) → K) a : K) (0 : K) → a = 0) (p : F[X])
    (hp :
      Eq.{u_2 + 1} (α := K) (↑((algebraMap F[X] ↥(ringOfIntegers F K) : (a : F[X]) → ↥(ringOfIntegers F K)) p) : K) 0),
    p = 0
⊢ p = 0

Tactic:
rw [injective_iff_map_eq_zero (algebraMap F[X] K)] at hinj

Premises used: Algebra.algebraMap, Polynomial, injective_iff_map_eq_zero
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
hinj : ∀ (a : F[X]), Eq.{u_2 + 1} (α := K) ((algebraMap F[X] K : (a : F[X]) → K) a : K) (0 : K) → a = 0
p : F[X]
hp : Eq.{u_2 + 1} (α := K) (↑((algebraMap F[X] ↥(ringOfIntegers F K) : (a : F[X]) → ↥(ringOfIntegers F K)) p) : K) 0
⊢ p = 0

Tactic:
hinj p hp
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
hinj : ∀ (a : F[X]), Eq.{u_2 + 1} (α := K) ((algebraMap F[X] K : (a : F[X]) → K) a : K) (0 : K) → a = 0
p : F[X]
hp : Eq.{u_2 + 1} (α := K) (↑((algebraMap F[X] ↥(ringOfIntegers F K) : (a : F[X]) → ↥(ringOfIntegers F K)) p) : K) 0
⊢ p = 0

Tactic:
exact hinj p hp
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
⊢ ¬IsField.{u_2} ↥(ringOfIntegers F K)

Tactic:
simpa [← (IsIntegralClosure.isIntegral_algebra F[X] K).isField_iff_isField
      (algebraMap_injective F K)] using
    Polynomial.not_isField F

Premises used: Polynomial.not_isField, FunctionField.ringOfIntegers.algebraMap_injective, Algebra.IsIntegral.isField_iff_isField
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
inst_5 : FunctionField F K
⊢ IsFractionRing (↥(ringOfIntegers F K)) K

Tactic:
integralClosure.isFractionRing_of_finite_extension F⟮X⟯ K

Premises used: Set.Mem, integralClosure.isFractionRing_of_finite_extension, RatFunc, FunctionField.ringOfIntegers
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
inst_5 : FunctionField F K
⊢ IsIntegrallyClosed.{u_2} ↥(ringOfIntegers F K)

Tactic:
integralClosure.isIntegrallyClosedOfFiniteExtension F⟮X⟯

Premises used: integralClosure.isIntegrallyClosedOfFiniteExtension, Set.Mem, RatFunc, FunctionField.ringOfIntegers
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
inst_5 : FunctionField F K
inst_6 : Algebra.IsSeparable.{u_1, u_2} F⟮X⟯ K
⊢ IsNoetherian.{u_1, u_2} F[X] ↥(ringOfIntegers F K)

Tactic:
IsIntegralClosure.isNoetherian _ F⟮X⟯ K _

Premises used: Set.Mem, RatFunc, integralClosure, FunctionField.ringOfIntegers, IsIntegralClosure.isNoetherian
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : Algebra.{u_1, u_2} F⟮X⟯ K
inst_4 : IsScalarTower.{u_1, u_1, u_2} F[X] F⟮X⟯ K
inst_5 : FunctionField F K
inst_6 : Algebra.IsSeparable.{u_1, u_2} F⟮X⟯ K
⊢ IsDedekindDomain.{u_2} ↥(ringOfIntegers F K)

Tactic:
IsIntegralClosure.isDedekindDomain F[X] F⟮X⟯ K _

Premises used: Polynomial, RatFunc, IsIntegralClosure.isDedekindDomain
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F_1 : Type u_1
K_1 : Type u_2
inst : Field F_1
inst_1 : Field K_1
F : Type u_3
K : Type u_4
inst_2 : Field F
inst_3 : Field K
inst_4 : Algebra.{u_3, u_4} F⟮X⟯ K
inst_5 : FunctionField F K
⊢ FiniteDimensional.{u_3, u_4} (↥F⟮ X⟯) K

Tactic:
have : Module.Finite (⊤ : IntermediateField F F⟮X⟯) F⟮X⟯ :=
    .top_left F⟮X⟯ F⟮X⟯
  RatFunc.adjoin_X (K := F) ▸ Module.Finite.trans F⟮X⟯ _

Premises used: Module.Finite.top_left, RatFunc.adjoin_X, Eq.rec, RatFunc, Module.Finite.trans, Eq.symm
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_3
K : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_3, u_4} F⟮X⟯ K
inst_3 : FunctionField F K
inst_4 : Algebra F K
inst_5 : IsScalarTower F F⟮X⟯ K
⊢ FiniteDimensional (↥F⟮((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X : K)⟯) K

Tactic:
.of_restrictScalars_finite F⟮(X : F⟮X⟯)⟯ _ _

Premises used: RatFunc.X, Membership.mem, Subtype, Module.Finite.of_restrictScalars_finite, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_3
K : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_3, u_4} F⟮X⟯ K
inst_3 : FunctionField F K
inst_4 : Algebra F K
inst_5 : IsScalarTower F F⟮X⟯ K
⊢ Algebra.IsAlgebraic (↥F⟮((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X : K)⟯) K

Tactic:
.tower_top (K := F⟮(X : F⟮X⟯)⟯) _

Premises used: Algebra.IsAlgebraic.tower_top
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_3
K : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_3, u_4} F⟮X⟯ K
inst_3 : FunctionField F K
inst_4 : Algebra F K
inst_5 : IsScalarTower F F⟮X⟯ K
⊢ Algebra.IsAlgebraic (↥F⟮((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X : K)⟯) K

Tactic:
exact .tower_top (K := F⟮(X : F⟮X⟯)⟯) _
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_3
K : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_3, u_4} F⟮X⟯ K
inst_3 : FunctionField F K
inst_4 : Algebra F K
inst_5 : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
⊢ IsAlgebraic.{u_4, u_4} ↥F⟮y⟯ (A := K) ((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X : K)

Tactic:
isAlgebraic_adjoin_iff.mpr (.adjoin_singleton transcendental_X hy
    (isAlgebraic_adjoin_iff.mp (Algebra.IsAlgebraic.isAlgebraic y)))

Premises used: IsAlgebraic.adjoin_singleton, Iff.mpr, Algebra.IsAlgebraic.isAlgebraic, RatFunc.transcendental_X, IntermediateField.isAlgebraic_adjoin_iff, Iff.mp
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_3
K : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_3, u_4} F⟮X⟯ K
inst_3 : FunctionField F K
inst_4 : Algebra F K
inst_5 : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X
Fyx : IntermediateField F K := restrictScalars F (L' := ↥F⟮y⟯) (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯
this_1 : Algebra ↥F⟮y⟯ ↥Fyx := Subalgebra.algebra (toSubalgebra (↥F⟮y⟯)⟮x⟯)
this_2 : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this_3 : SMul ↥F⟮y⟯ ↥Fyx := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮y⟯) DivisionSemiring.toSemiring _
this_4 : Algebra ↥F⟮x⟯ ↥Fxy := Subalgebra.algebra (toSubalgebra (↥F⟮x⟯)⟮y⟯)
this_5 : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this_6 : SMul ↥F⟮x⟯ ↥Fxy := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮x⟯) DivisionSemiring.toSemiring _
this : FiniteDimensional.{u_4, u_4} ↥F⟮y⟯ ↥Fyx
⊢ FiniteDimensional (↥F⟮((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X : K)⟯) K

Tactic:
have := FiniteDimensional.adjoin_algebraMap_X (F := F) (K := K)
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_3
K : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_3, u_4} F⟮X⟯ K
inst_3 : FunctionField F K
inst_4 : Algebra F K
inst_5 : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X
Fyx : IntermediateField F K := restrictScalars F (L' := ↥F⟮y⟯) (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯
this_1 : Algebra ↥F⟮y⟯ ↥Fyx := Subalgebra.algebra (toSubalgebra (↥F⟮y⟯)⟮x⟯)
this_2 : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this_3 : SMul ↥F⟮y⟯ ↥Fyx := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮y⟯) DivisionSemiring.toSemiring _
this_4 : Algebra ↥F⟮x⟯ ↥Fxy := Subalgebra.algebra (toSubalgebra (↥F⟮x⟯)⟮y⟯)
this_5 : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this_6 : SMul ↥F⟮x⟯ ↥Fxy := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮x⟯) DivisionSemiring.toSemiring _
this_7 : FiniteDimensional.{u_4, u_4} ↥F⟮y⟯ ↥Fyx
this : FiniteDimensional (↥F⟮((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X : K)⟯) K
unfold : FiniteDimensional (↥(restrictScalars F (L' := ↥F⟮y⟯) (↥F⟮y⟯)⟮x⟯)) K
⊢ FiniteDimensional (↥Fyx) K

Tactic:
unfold Fyx
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_3
K : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_3, u_4} F⟮X⟯ K
inst_3 : FunctionField F K
inst_4 : Algebra F K
inst_5 : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X
Fyx : IntermediateField F K := restrictScalars F (L' := ↥F⟮y⟯) (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯
this_1 : Algebra ↥F⟮y⟯ ↥Fyx := Subalgebra.algebra (toSubalgebra (↥F⟮y⟯)⟮x⟯)
this_2 : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this_3 : SMul ↥F⟮y⟯ ↥Fyx := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮y⟯) DivisionSemiring.toSemiring _
this_4 : Algebra ↥F⟮x⟯ ↥Fxy := Subalgebra.algebra (toSubalgebra (↥F⟮x⟯)⟮y⟯)
this_5 : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this_6 : SMul ↥F⟮x⟯ ↥Fxy := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮x⟯) DivisionSemiring.toSemiring _
this_7 : FiniteDimensional.{u_4, u_4} ↥F⟮y⟯ ↥Fyx
this : FiniteDimensional (↥F⟮((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X : K)⟯) K
rw : FiniteDimensional (↥(restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯)) K
⊢ FiniteDimensional (↥(restrictScalars F (L' := ↥F⟮y⟯) (↥F⟮y⟯)⟮x⟯)) K

Tactic:
rw [adjoin_simple_comm]

Premises used: IntermediateField.adjoin_simple_comm
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_3
K : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_3, u_4} F⟮X⟯ K
inst_3 : FunctionField F K
inst_4 : Algebra F K
inst_5 : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X
Fyx : IntermediateField F K := restrictScalars F (L' := ↥F⟮y⟯) (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯
this_1 : Algebra ↥F⟮y⟯ ↥Fyx := Subalgebra.algebra (toSubalgebra (↥F⟮y⟯)⟮x⟯)
this_2 : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this_3 : SMul ↥F⟮y⟯ ↥Fyx := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮y⟯) DivisionSemiring.toSemiring _
this_4 : Algebra ↥F⟮x⟯ ↥Fxy := Subalgebra.algebra (toSubalgebra (↥F⟮x⟯)⟮y⟯)
this_5 : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this_6 : SMul ↥F⟮x⟯ ↥Fxy := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮x⟯) DivisionSemiring.toSemiring _
this_7 : FiniteDimensional.{u_4, u_4} ↥F⟮y⟯ ↥Fyx
this : FiniteDimensional (↥F⟮((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X : K)⟯) K
⊢ IsScalarTower (↥F⟮x⟯) (↥Fxy) K

Tactic:
have : IsScalarTower F⟮x⟯ Fxy K := isScalarTower_mid' F⟮x⟯⟮y⟯
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_3
K : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_3, u_4} F⟮X⟯ K
inst_3 : FunctionField F K
inst_4 : Algebra F K
inst_5 : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X
Fyx : IntermediateField F K := restrictScalars F (L' := ↥F⟮y⟯) (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯
this_1 : Algebra ↥F⟮y⟯ ↥Fyx := Subalgebra.algebra (toSubalgebra (↥F⟮y⟯)⟮x⟯)
this_2 : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this_3 : SMul ↥F⟮y⟯ ↥Fyx := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮y⟯) DivisionSemiring.toSemiring _
this_4 : Algebra ↥F⟮x⟯ ↥Fxy := Subalgebra.algebra (toSubalgebra (↥F⟮x⟯)⟮y⟯)
this_5 : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this_6 : SMul ↥F⟮x⟯ ↥Fxy := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮x⟯) DivisionSemiring.toSemiring _
this_7 : FiniteDimensional.{u_4, u_4} ↥F⟮y⟯ ↥Fyx
this_8 : FiniteDimensional (↥F⟮((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X : K)⟯) K
this : IsScalarTower (↥F⟮x⟯) (↥Fxy) K
⊢ FiniteDimensional (↥(restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯)) K

Tactic:
.right F⟮x⟯ Fxy K

Premises used: Set.Mem, Membership.mem, Subtype, FiniteDimensional.right, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_3
K : Type u_4
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_3, u_4} F⟮X⟯ K
inst_3 : FunctionField F K
inst_4 : Algebra F K
inst_5 : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X
Fyx : IntermediateField F K := restrictScalars F (L' := ↥F⟮y⟯) (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯
this_1 : Algebra ↥F⟮y⟯ ↥Fyx := Subalgebra.algebra (toSubalgebra (↥F⟮y⟯)⟮x⟯)
this_2 : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this_3 : SMul ↥F⟮y⟯ ↥Fyx := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮y⟯) DivisionSemiring.toSemiring _
this_4 : Algebra ↥F⟮x⟯ ↥Fxy := Subalgebra.algebra (toSubalgebra (↥F⟮x⟯)⟮y⟯)
this_5 : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this_6 : SMul ↥F⟮x⟯ ↥Fxy := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring F⟮x⟯) DivisionSemiring.toSemiring _
this_7 : FiniteDimensional.{u_4, u_4} ↥F⟮y⟯ ↥Fyx
this_8 : FiniteDimensional (↥F⟮((algebraMap F⟮X⟯ K : (a : F⟮X⟯) → K) X : K)⟯) K
this : IsScalarTower (↥F⟮x⟯) (↥Fxy) K
⊢ FiniteDimensional (↥(restrictScalars F (L' := ↥F⟮x⟯) (↥F⟮x⟯)⟮y⟯)) K

Tactic:
exact .right F⟮x⟯ Fxy K
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : FaithfulSMul.{u_1, u_2} F[X] K
inst_4 : FunctionField F K
E : Type u_3
inst_5 : Field E
inst_6 : Algebra F E
inst_7 : Algebra.{u_3, u_2} E[X] K
inst_8 : FaithfulSMul.{u_3, u_2} E[X] K
inst_9 : IsScalarTower.{u_1, u_3, u_2} F[X] E[X] K
⊢ FiniteDimensional.{u_1, u_3} F⟮X⟯ E⟮X⟯

Tactic:
.equiv (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F⟮X⟯ E⟮X⟯ K)).toLinearEquiv.symm

Premises used: AlgEquiv.ofInjectiveField, LinearEquiv.symm, IsScalarTower.toAlgHom, RatFunc, AlgEquiv.toLinearEquiv, Module.Finite.equiv
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : FaithfulSMul.{u_1, u_2} F[X] K
inst_4 : FunctionField F K
E : Type u_3
inst_5 : Field E
inst_6 : Algebra F E
inst_7 : Algebra.{u_3, u_2} E[X] K
inst_8 : FaithfulSMul.{u_3, u_2} E[X] K
inst_9 : IsScalarTower.{u_1, u_3, u_2} F[X] E[X] K
inst_10 : Algebra.IsAlgebraic F E
⊢ FiniteDimensional F E

Tactic:
have := finiteDimensional_ratFunc_of_constantExtension (F := F) (E := E) K
  Module.finite_of_finrank_pos ((finrank_ratFunc_ratFunc F E) ▸ Module.finrank_pos)

Premises used: Module.finite_of_finrank_pos, FunctionField.finiteDimensional_ratFunc_of_constantExtension, Eq.rec, RatFunc.finrank_ratFunc_ratFunc, Module.finrank_pos
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : FaithfulSMul.{u_1, u_2} F[X] K
inst_4 : FunctionField F K
inst_5 : Algebra F K
E : IntermediateField F K
inst_6 : Algebra (↥E)[X] K
inst_7 : FaithfulSMul (↥E)[X] K
inst_8 : IsScalarTower.{u_1, u_2, u_2} F[X] (↥E)[X] K
⊢ FiniteDimensional.{u_1, u_2} F⟮X⟯ (↥E)⟮X⟯

Tactic:
finiteDimensional_ratFunc_of_constantExtension K

Premises used: FunctionField.finiteDimensional_ratFunc_of_constantExtension
-- Module: Mathlib.NumberTheory.FunctionField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} F[X] K
inst_3 : FaithfulSMul.{u_1, u_2} F[X] K
inst_4 : FunctionField F K
inst_5 : Algebra F K
E : IntermediateField F K
inst_6 : Algebra (↥E)[X] K
inst_7 : FaithfulSMul (↥E)[X] K
inst_8 : IsScalarTower.{u_1, u_2, u_2} F[X] (↥E)[X] K
inst_9 : Algebra.IsAlgebraic.{u_1, u_2} F ↥E
⊢ FiniteDimensional.{u_1, u_2} F ↥E

Tactic:
finiteDimensional_of_constantExtension K

Premises used: Set.Mem, FunctionField.finiteDimensional_of_constantExtension