-- 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:
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
⊢ FunctionField Fq F ↔ FiniteDimensional Fqt F

Tactic:
have : ∀ (c) (x : F), e c • x = c • x := by
  intro c x
  rw [Algebra.smul_def, Algebra.smul_def]
  congr
  refine congr_fun (f := fun c => algebraMap Fqt F (e c)) ?_ c refine IsLocalization.ext (nonZeroDivisors Fq[X]) _ _ ?_ ?_ ?_ ?_ ?_ <;> intros <;>
    simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]

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
this : ∀ (c : RatFunc Fq) (x : F), e c • x = c • x
⊢ FunctionField 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
⊢ FunctionField Fq F

Tactic:
refine FiniteDimensional.of_fintype_basis (b.mapCoeffs e.symm ?_)

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
⊢ FunctionField Fq F ↔ FiniteDimensional Fqt F

Tactic:
let e := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt

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
⊢ FunctionField Fq F ↔ FiniteDimensional Fqt F

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
⊢ (algebraMap Fqt F) (e c) * x = (algebraMap (RatFunc Fq) F) c * x

Tactic:
congr

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
⊢ (algebraMap Fqt F) (e c) = (algebraMap (RatFunc Fq) F) c

Proof state:
case h.e'_3.h.e'_5
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
⊢ c = e (e.symm c)

Tactic:
simp only [e.apply_symm_apply]

Result:
no goals

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:
convert (this (e.symm c) x).symm

Result:
case h.e'_3.h.e'_5
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
⊢ c = e (e.symm c)

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
⊢ (fun c => (algebraMap Fqt F) (e c)) = ⇑(algebraMap (RatFunc Fq) F)

Tactic:
refine IsLocalization.ext (nonZeroDivisors Fq[X]) _ _ ?_ ?_ ?_ ?_ ?_ <;> intros <;>
  simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]

Result:
no goals