-- Mathlib/NumberTheory/FunctionField.lean
theorem functionField_iff (Fqt : Type*) [Field Fqt] [Algebra Fq[X] Fqt]
    [IsFractionRing Fq[X] Fqt] [Algebra (RatFunc Fq) F] [Algebra Fqt F] [Algebra Fq[X] F]
    [IsScalarTower Fq[X] Fqt F] [IsScalarTower Fq[X] (RatFunc Fq) F] :
    FunctionField Fq F ↔ FiniteDimensional Fqt F

Proof state:
case mp
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), e c • x = c • x
h : FunctionField Fq F
b : Basis (Fin (Module.finrank (RatFunc Fq) F)) (RatFunc Fq) F := Module.finBasis (RatFunc Fq) F
⊢ FiniteDimensional Fqt F

Tactic:
exact FiniteDimensional.of_fintype_basis (b.mapCoeffs e this)

Result:
no goals

Proof state:
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
⊢ ∀ (c : RatFunc Fq) (x : F), e c • x = c • x

Tactic:
intro c x

Result:
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ e c • x = c • x

Proof state:
case mp
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), e c • x = c • x
h : FunctionField Fq F
⊢ FiniteDimensional Fqt F

Tactic:
let b := Module.finBasis (RatFunc Fq) F

Result:
case mp
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), e c • x = c • x
h : FunctionField Fq F
b : Basis (Fin (Module.finrank (RatFunc Fq) F)) (RatFunc Fq) F := Module.finBasis (RatFunc Fq) F
⊢ FiniteDimensional Fqt F

Proof state:
case mpr
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), e c • x = c • x
h : FiniteDimensional Fqt F
b : Basis (Fin (Module.finrank Fqt F)) Fqt F := Module.finBasis Fqt F
⊢ ∀ (c : Fqt) (x : F), ↑e.symm c • x = c • x

Tactic:
intro c x

Result:
case mpr
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), e c • x = c • x
h : FiniteDimensional Fqt F
b : Basis (Fin (Module.finrank Fqt F)) Fqt F := Module.finBasis Fqt F
c : Fqt
x : F
⊢ ↑e.symm c • x = c • x

Proof state:
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), e c • x = c • x
⊢ FunctionField Fq F ↔ FiniteDimensional Fqt F

Tactic:
constructor <;> intro h

Result:
case mp
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), e c • x = c • x
h : FunctionField Fq F
⊢ FiniteDimensional Fqt F

case mpr
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
this : ∀ (c : RatFunc Fq) (x : F), e c • x = c • x
h : FiniteDimensional Fqt F
⊢ FunctionField Fq F

Proof state:
case e_a
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ (algebraMap Fqt F) (e c) = (algebraMap (RatFunc Fq) F) c

Tactic:
refine congr_fun (f := fun c => algebraMap Fqt F (e c)) ?_ c

Result:
case e_a
Fq : Type u_1
F : Type u_2
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_3
inst✝⁷ : Field Fqt
inst✝⁶ : Algebra Fq[X] Fqt
inst✝⁵ : IsFractionRing Fq[X] Fqt
inst✝⁴ : Algebra (RatFunc Fq) F
inst✝³ : Algebra Fqt F
inst✝² : Algebra Fq[X] F
inst✝¹ : IsScalarTower Fq[X] Fqt F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
c : RatFunc Fq
x : F
⊢ (fun c => (algebraMap Fqt F) (e c)) = ⇑(algebraMap (RatFunc Fq) F)