[GOAL]
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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
[PROOFSTEP]
let e := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
[GOAL]
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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
[PROOFSTEP]
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 [AlgEquiv.map_one, RingHom.map_one, AlgEquiv.map_mul, RingHom.map_mul, AlgEquiv.commutes, ←
      IsScalarTower.algebraMap_apply]
[GOAL]
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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
[PROOFSTEP]
intro c x
[GOAL]
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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
[PROOFSTEP]
rw [Algebra.smul_def, Algebra.smul_def]
[GOAL]
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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 ((fun x => Fqt) c) F) (↑e c) * x = ↑(algebraMap (RatFunc Fq) F) c * x
[PROOFSTEP]
congr
[GOAL]
case e_a
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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 ((fun x => Fqt) c) F) (↑e c) = ↑(algebraMap (RatFunc Fq) F) c
[PROOFSTEP]
refine' congr_fun (f := fun c => algebraMap Fqt F (e c)) _ c
[GOAL]
case e_a
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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)
[PROOFSTEP]
refine' IsLocalization.ext (nonZeroDivisors Fq[X]) _ _ _ _ _ _ _
[GOAL]
case e_a.refine'_1
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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 1) = 1
[PROOFSTEP]
intros
[GOAL]
case e_a.refine'_2
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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 (RatFunc Fq) F) 1 = 1
[PROOFSTEP]
intros
[GOAL]
case e_a.refine'_3
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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
⊢ ∀ (a b : RatFunc Fq), ↑(algebraMap Fqt F) (↑e (a * b)) = ↑(algebraMap Fqt F) (↑e a) * ↑(algebraMap Fqt F) (↑e b)
[PROOFSTEP]
intros
[GOAL]
case e_a.refine'_4
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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
⊢ ∀ (a b : RatFunc Fq),
    ↑(algebraMap (RatFunc Fq) F) (a * b) = ↑(algebraMap (RatFunc Fq) F) a * ↑(algebraMap (RatFunc Fq) F) b
[PROOFSTEP]
intros
[GOAL]
case e_a.refine'_5
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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
⊢ ∀ (a : Fq[X]),
    ↑(algebraMap Fqt F) (↑e (↑(algebraMap Fq[X] (RatFunc Fq)) a)) =
      ↑(algebraMap (RatFunc Fq) F) (↑(algebraMap Fq[X] (RatFunc Fq)) a)
[PROOFSTEP]
intros
[GOAL]
case e_a.refine'_1
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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 1) = 1
[PROOFSTEP]
simp only [AlgEquiv.map_one, RingHom.map_one, AlgEquiv.map_mul, RingHom.map_mul, AlgEquiv.commutes, ←
  IsScalarTower.algebraMap_apply]
[GOAL]
case e_a.refine'_2
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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 (RatFunc Fq) F) 1 = 1
[PROOFSTEP]
simp only [AlgEquiv.map_one, RingHom.map_one, AlgEquiv.map_mul, RingHom.map_mul, AlgEquiv.commutes, ←
  IsScalarTower.algebraMap_apply]
[GOAL]
case e_a.refine'_3
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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
a✝ b✝ : RatFunc Fq
⊢ ↑(algebraMap Fqt F) (↑e (a✝ * b✝)) = ↑(algebraMap Fqt F) (↑e a✝) * ↑(algebraMap Fqt F) (↑e b✝)
[PROOFSTEP]
simp only [AlgEquiv.map_one, RingHom.map_one, AlgEquiv.map_mul, RingHom.map_mul, AlgEquiv.commutes, ←
  IsScalarTower.algebraMap_apply]
[GOAL]
case e_a.refine'_4
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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
a✝ b✝ : RatFunc Fq
⊢ ↑(algebraMap (RatFunc Fq) F) (a✝ * b✝) = ↑(algebraMap (RatFunc Fq) F) a✝ * ↑(algebraMap (RatFunc Fq) F) b✝
[PROOFSTEP]
simp only [AlgEquiv.map_one, RingHom.map_one, AlgEquiv.map_mul, RingHom.map_mul, AlgEquiv.commutes, ←
  IsScalarTower.algebraMap_apply]
[GOAL]
case e_a.refine'_5
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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
a✝ : Fq[X]
⊢ ↑(algebraMap Fqt F) (↑e (↑(algebraMap Fq[X] (RatFunc Fq)) a✝)) =
    ↑(algebraMap (RatFunc Fq) F) (↑(algebraMap Fq[X] (RatFunc Fq)) a✝)
[PROOFSTEP]
simp only [AlgEquiv.map_one, RingHom.map_one, AlgEquiv.map_mul, RingHom.map_mul, AlgEquiv.commutes, ←
  IsScalarTower.algebraMap_apply]
[GOAL]
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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
[PROOFSTEP]
constructor
[GOAL]
case mp
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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
[PROOFSTEP]
intro h
[GOAL]
case mpr
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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
⊢ FiniteDimensional Fqt F → FunctionField Fq F
[PROOFSTEP]
intro h
[GOAL]
case mp
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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
[PROOFSTEP]
let b := FiniteDimensional.finBasis (RatFunc Fq) F
[GOAL]
case mp
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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 (FiniteDimensional.finrank (RatFunc Fq) F)) (RatFunc Fq) F := FiniteDimensional.finBasis (RatFunc Fq) F
⊢ FiniteDimensional Fqt F
[PROOFSTEP]
exact FiniteDimensional.of_fintype_basis (b.mapCoeffs e this)
[GOAL]
case mpr
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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
[PROOFSTEP]
let b := FiniteDimensional.finBasis Fqt F
[GOAL]
case mpr
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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 (FiniteDimensional.finrank Fqt F)) Fqt F := FiniteDimensional.finBasis Fqt F
⊢ FunctionField Fq F
[PROOFSTEP]
refine' FiniteDimensional.of_fintype_basis (b.mapCoeffs e.symm _)
[GOAL]
case mpr
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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 (FiniteDimensional.finrank Fqt F)) Fqt F := FiniteDimensional.finBasis Fqt F
⊢ ∀ (c : Fqt) (x : F), ↑↑(AlgEquiv.symm e) c • x = c • x
[PROOFSTEP]
intro c x
[GOAL]
case mpr
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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 (FiniteDimensional.finrank Fqt F)) Fqt F := FiniteDimensional.finBasis Fqt F
c : Fqt
x : F
⊢ ↑↑(AlgEquiv.symm e) c • x = c • x
[PROOFSTEP]
convert (this (e.symm c) x).symm
[GOAL]
case h.e'_3.h.e'_5
Fq F : Type
inst✝⁹ : Field Fq
inst✝⁸ : Field F
Fqt : Type u_1
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 (FiniteDimensional.finrank Fqt F)) Fqt F := FiniteDimensional.finBasis Fqt F
c : Fqt
x : F
⊢ c = ↑e (↑(AlgEquiv.symm e) c)
[PROOFSTEP]
simp only [e.apply_symm_apply]
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ Function.Injective ↑(algebraMap Fq[X] F)
[PROOFSTEP]
rw [IsScalarTower.algebraMap_eq Fq[X] (RatFunc Fq) F]
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ Function.Injective ↑(RingHom.comp (algebraMap (RatFunc Fq) F) (algebraMap Fq[X] (RatFunc Fq)))
[PROOFSTEP]
exact (algebraMap (RatFunc Fq) F).injective.comp (IsFractionRing.injective Fq[X] (RatFunc Fq))
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ Function.Injective ↑(algebraMap Fq[X] { x // x ∈ ringOfIntegers Fq F })
[PROOFSTEP]
have hinj : Function.Injective (⇑(algebraMap Fq[X] F)) :=
  by
  rw [IsScalarTower.algebraMap_eq Fq[X] (RatFunc Fq) F]
  exact (algebraMap (RatFunc Fq) F).injective.comp (IsFractionRing.injective Fq[X] (RatFunc Fq))
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ Function.Injective ↑(algebraMap Fq[X] F)
[PROOFSTEP]
rw [IsScalarTower.algebraMap_eq Fq[X] (RatFunc Fq) F]
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ Function.Injective ↑(RingHom.comp (algebraMap (RatFunc Fq) F) (algebraMap Fq[X] (RatFunc Fq)))
[PROOFSTEP]
exact (algebraMap (RatFunc Fq) F).injective.comp (IsFractionRing.injective Fq[X] (RatFunc Fq))
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
hinj : Function.Injective ↑(algebraMap Fq[X] F)
⊢ Function.Injective ↑(algebraMap Fq[X] { x // x ∈ ringOfIntegers Fq F })
[PROOFSTEP]
rw [injective_iff_map_eq_zero (algebraMap Fq[X] (↥(ringOfIntegers Fq F)))]
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
hinj : Function.Injective ↑(algebraMap Fq[X] F)
⊢ ∀ (a : Fq[X]), ↑(algebraMap Fq[X] { x // x ∈ ringOfIntegers Fq F }) a = 0 → a = 0
[PROOFSTEP]
intro p hp
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
hinj : Function.Injective ↑(algebraMap Fq[X] F)
p : Fq[X]
hp : ↑(algebraMap Fq[X] { x // x ∈ ringOfIntegers Fq F }) p = 0
⊢ p = 0
[PROOFSTEP]
rw [← Subtype.coe_inj, Subalgebra.coe_zero] at hp
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
hinj : Function.Injective ↑(algebraMap Fq[X] F)
p : Fq[X]
hp : ↑(↑(algebraMap Fq[X] { x // x ∈ ringOfIntegers Fq F }) p) = 0
⊢ p = 0
[PROOFSTEP]
rw [injective_iff_map_eq_zero (algebraMap Fq[X] F)] at hinj
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
hinj : ∀ (a : Fq[X]), ↑(algebraMap Fq[X] F) a = 0 → a = 0
p : Fq[X]
hp : ↑(↑(algebraMap Fq[X] { x // x ∈ ringOfIntegers Fq F }) p) = 0
⊢ p = 0
[PROOFSTEP]
exact hinj p hp
[GOAL]
Fq F : Type
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ ¬IsField { x // x ∈ ringOfIntegers Fq F }
[PROOFSTEP]
simpa [← (IsIntegralClosure.isIntegral_algebra Fq[X] F).isField_iff_isField (algebraMap_injective Fq F)] using
  Polynomial.not_isField Fq
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
⊢ ↑(↑Multiplicative.ofAdd (RatFunc.intDegree 1)) = 1
[PROOFSTEP]
rw [RatFunc.intDegree_one, ofAdd_zero, WithZero.coe_one]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
⊢ inftyValuationDef Fq (x * y) = inftyValuationDef Fq x * inftyValuationDef Fq y
[PROOFSTEP]
rw [inftyValuationDef, inftyValuationDef, inftyValuationDef]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
⊢ (if x * y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree (x * y)))) =
    (if x = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree x))) *
      if y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree y))
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ (if x * y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree (x * y)))) =
    (if x = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree x))) *
      if y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree y))
[PROOFSTEP]
rw [hx, zero_mul, if_pos (Eq.refl _), zero_mul]
[GOAL]
case neg
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
⊢ (if x * y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree (x * y)))) =
    (if x = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree x))) *
      if y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree y))
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree (x * y)))) =
    (if x = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree x))) *
      if y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree y))
[PROOFSTEP]
rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]
[GOAL]
case neg
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree (x * y)))) =
    (if x = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree x))) *
      if y = 0 then 0 else ↑(↑Multiplicative.ofAdd (RatFunc.intDegree y))
[PROOFSTEP]
rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithZero.coe_mul, WithZero.coe_inj, ← ofAdd_add,
  RatFunc.intDegree_mul hx hy]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
⊢ inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
rw [hx, zero_add]
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ inftyValuationDef Fq y ≤ max (inftyValuationDef Fq 0) (inftyValuationDef Fq y)
[PROOFSTEP]
conv_rhs => rw [inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
| max (inftyValuationDef Fq 0) (inftyValuationDef Fq y)
[PROOFSTEP]
rw [inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
| max (inftyValuationDef Fq 0) (inftyValuationDef Fq y)
[PROOFSTEP]
rw [inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
| max (inftyValuationDef Fq 0) (inftyValuationDef Fq y)
[PROOFSTEP]
rw [inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ inftyValuationDef Fq y ≤ max 0 (inftyValuationDef Fq y)
[PROOFSTEP]
rw [max_eq_right (WithZero.zero_le (inftyValuationDef Fq y))]
[GOAL]
case neg
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
⊢ inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
rw [hy, add_zero]
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ inftyValuationDef Fq x ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq 0)
[PROOFSTEP]
conv_rhs => rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
| max (inftyValuationDef Fq x) (inftyValuationDef Fq 0)
[PROOFSTEP]
rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
| max (inftyValuationDef Fq x) (inftyValuationDef Fq 0)
[PROOFSTEP]
rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
| max (inftyValuationDef Fq x) (inftyValuationDef Fq 0)
[PROOFSTEP]
rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ inftyValuationDef Fq x ≤ max 0 (inftyValuationDef Fq x)
[PROOFSTEP]
rw [max_eq_right (WithZero.zero_le (inftyValuationDef Fq x))]
[GOAL]
case neg
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
⊢ inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
by_cases hxy : x + y = 0
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
rw [inftyValuationDef, if_pos hxy]
[GOAL]
case pos
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ 0 ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
exact zero_le'
[GOAL]
case neg
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)
[PROOFSTEP]
rw [inftyValuationDef, inftyValuationDef, inftyValuationDef, if_neg hx, if_neg hy, if_neg hxy]
[GOAL]
case neg
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ ↑(↑Multiplicative.ofAdd (RatFunc.intDegree (x + y))) ≤
    max ↑(↑Multiplicative.ofAdd (RatFunc.intDegree x)) ↑(↑Multiplicative.ofAdd (RatFunc.intDegree y))
[PROOFSTEP]
rw [le_max_iff, WithZero.coe_le_coe, Multiplicative.ofAdd_le, WithZero.coe_le_coe, Multiplicative.ofAdd_le, ←
  le_max_iff]
[GOAL]
case neg
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ RatFunc.intDegree (x + y) ≤ max (RatFunc.intDegree x) (RatFunc.intDegree y)
[PROOFSTEP]
exact RatFunc.intDegree_add_le hy hxy
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
x : RatFunc Fq
hx : x ≠ 0
⊢ inftyValuationDef Fq x = ↑(↑Multiplicative.ofAdd (RatFunc.intDegree x))
[PROOFSTEP]
rw [inftyValuationDef, if_neg hx]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
k : Fq
hk : k ≠ 0
⊢ inftyValuationDef Fq (↑RatFunc.C k) = ↑(↑Multiplicative.ofAdd 0)
[PROOFSTEP]
have hCk : RatFunc.C k ≠ 0 := (map_ne_zero _).mpr hk
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
k : Fq
hk : k ≠ 0
hCk : ↑RatFunc.C k ≠ 0
⊢ inftyValuationDef Fq (↑RatFunc.C k) = ↑(↑Multiplicative.ofAdd 0)
[PROOFSTEP]
rw [inftyValuationDef, if_neg hCk, RatFunc.intDegree_C]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
⊢ inftyValuationDef Fq RatFunc.X = ↑(↑Multiplicative.ofAdd 1)
[PROOFSTEP]
rw [inftyValuationDef, if_neg RatFunc.X_ne_zero, RatFunc.intDegree_X]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
p : Fq[X]
hp : p ≠ 0
⊢ inftyValuationDef Fq (↑(algebraMap Fq[X] (RatFunc Fq)) p) = ↑(↑Multiplicative.ofAdd ↑(Polynomial.natDegree p))
[PROOFSTEP]
have hp' : algebraMap Fq[X] (RatFunc Fq) p ≠ 0 := by rw [Ne.def, RatFunc.algebraMap_eq_zero_iff]; exact hp
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
p : Fq[X]
hp : p ≠ 0
⊢ ↑(algebraMap Fq[X] (RatFunc Fq)) p ≠ 0
[PROOFSTEP]
rw [Ne.def, RatFunc.algebraMap_eq_zero_iff]
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
p : Fq[X]
hp : p ≠ 0
⊢ ¬p = 0
[PROOFSTEP]
exact hp
[GOAL]
Fq F : Type
inst✝² : Field Fq
inst✝¹ : Field F
inst✝ : DecidableEq (RatFunc Fq)
p : Fq[X]
hp : p ≠ 0
hp' : ↑(algebraMap Fq[X] (RatFunc Fq)) p ≠ 0
⊢ inftyValuationDef Fq (↑(algebraMap Fq[X] (RatFunc Fq)) p) = ↑(↑Multiplicative.ofAdd ↑(Polynomial.natDegree p))
[PROOFSTEP]
rw [inftyValuationDef, if_neg hp', RatFunc.intDegree_polynomial]


[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ legendreSym p 2 = ↑χ₈ ↑p
[PROOFSTEP]
have : (2 : ZMod p) = (2 : ℤ) := by norm_cast
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ 2 = ↑2
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : 2 = ↑2
⊢ legendreSym p 2 = ↑χ₈ ↑p
[PROOFSTEP]
rw [legendreSym, ← this, quadraticChar_two ((ringChar_zmod_n p).substr hp), card p]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ legendreSym p (-2) = ↑χ₈' ↑p
[PROOFSTEP]
have : (-2 : ZMod p) = (-2 : ℤ) := by norm_cast
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ -2 = ↑(-2)
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : -2 = ↑(-2)
⊢ legendreSym p (-2) = ↑χ₈' ↑p
[PROOFSTEP]
rw [legendreSym, ← this, quadraticChar_neg_two ((ringChar_zmod_n p).substr hp), card p]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ IsSquare 2 ↔ p % 8 = 1 ∨ p % 8 = 7
[PROOFSTEP]
rw [FiniteField.isSquare_two_iff, card p]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
[PROOFSTEP]
have h₁ := Prime.mod_two_eq_one_iff_ne_two.mpr hp
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 2 = 1
⊢ p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
[PROOFSTEP]
rw [← mod_mod_of_dvd p (by norm_num : 2 ∣ 8)] at h₁
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 2 = 1
⊢ 2 ∣ 8
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 8 % 2 = 1
⊢ p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
[PROOFSTEP]
have h₂ := mod_lt p (by norm_num : 0 < 8)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 8 % 2 = 1
⊢ 0 < 8
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 8 % 2 = 1
h₂ : p % 8 < 8
⊢ p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
[PROOFSTEP]
revert h₂ h₁
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 % 2 = 1 → p % 8 < 8 → (p % 8 ≠ 3 ∧ p % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7)
[PROOFSTEP]
generalize p % 8 = m
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
m : ℕ
⊢ m % 2 = 1 → m < 8 → (m ≠ 3 ∧ m ≠ 5 ↔ m = 1 ∨ m = 7)
[PROOFSTEP]
clear! p
[GOAL]
m : ℕ
⊢ m % 2 = 1 → m < 8 → (m ≠ 3 ∧ m ≠ 5 ↔ m = 1 ∨ m = 7)
[PROOFSTEP]
intros
[GOAL]
m : ℕ
h₁✝ : m % 2 = 1
h₂✝ : m < 8
⊢ m ≠ 3 ∧ m ≠ 5 ↔ m = 1 ∨ m = 7
[PROOFSTEP]
interval_cases m
[GOAL]
case «0»
m : ℕ
h₁✝ : 0 % 2 = 1
h₂✝ : 0 < 8
⊢ 0 ≠ 3 ∧ 0 ≠ 5 ↔ 0 = 1 ∨ 0 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «1»
m : ℕ
h₁✝ : 1 % 2 = 1
h₂✝ : 1 < 8
⊢ 1 ≠ 3 ∧ 1 ≠ 5 ↔ 1 = 1 ∨ 1 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «2»
m : ℕ
h₁✝ : 2 % 2 = 1
h₂✝ : 2 < 8
⊢ 2 ≠ 3 ∧ 2 ≠ 5 ↔ 2 = 1 ∨ 2 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «3»
m : ℕ
h₁✝ : 3 % 2 = 1
h₂✝ : 3 < 8
⊢ 3 ≠ 3 ∧ 3 ≠ 5 ↔ 3 = 1 ∨ 3 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «4»
m : ℕ
h₁✝ : 4 % 2 = 1
h₂✝ : 4 < 8
⊢ 4 ≠ 3 ∧ 4 ≠ 5 ↔ 4 = 1 ∨ 4 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «5»
m : ℕ
h₁✝ : 5 % 2 = 1
h₂✝ : 5 < 8
⊢ 5 ≠ 3 ∧ 5 ≠ 5 ↔ 5 = 1 ∨ 5 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «6»
m : ℕ
h₁✝ : 6 % 2 = 1
h₂✝ : 6 < 8
⊢ 6 ≠ 3 ∧ 6 ≠ 5 ↔ 6 = 1 ∨ 6 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «7»
m : ℕ
h₁✝ : 7 % 2 = 1
h₂✝ : 7 < 8
⊢ 7 ≠ 3 ∧ 7 ≠ 5 ↔ 7 = 1 ∨ 7 = 7
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ IsSquare (-2) ↔ p % 8 = 1 ∨ p % 8 = 3
[PROOFSTEP]
rw [FiniteField.isSquare_neg_two_iff, card p]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
[PROOFSTEP]
have h₁ := Prime.mod_two_eq_one_iff_ne_two.mpr hp
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 2 = 1
⊢ p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
[PROOFSTEP]
rw [← mod_mod_of_dvd p (by norm_num : 2 ∣ 8)] at h₁
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 2 = 1
⊢ 2 ∣ 8
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 8 % 2 = 1
⊢ p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
[PROOFSTEP]
have h₂ := mod_lt p (by norm_num : 0 < 8)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 8 % 2 = 1
⊢ 0 < 8
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
h₁ : p % 8 % 2 = 1
h₂ : p % 8 < 8
⊢ p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
[PROOFSTEP]
revert h₂ h₁
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ p % 8 % 2 = 1 → p % 8 < 8 → (p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3)
[PROOFSTEP]
generalize p % 8 = m
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
m : ℕ
⊢ m % 2 = 1 → m < 8 → (m ≠ 5 ∧ m ≠ 7 ↔ m = 1 ∨ m = 3)
[PROOFSTEP]
clear! p
[GOAL]
m : ℕ
⊢ m % 2 = 1 → m < 8 → (m ≠ 5 ∧ m ≠ 7 ↔ m = 1 ∨ m = 3)
[PROOFSTEP]
intros
[GOAL]
m : ℕ
h₁✝ : m % 2 = 1
h₂✝ : m < 8
⊢ m ≠ 5 ∧ m ≠ 7 ↔ m = 1 ∨ m = 3
[PROOFSTEP]
interval_cases m
[GOAL]
case «0»
m : ℕ
h₁✝ : 0 % 2 = 1
h₂✝ : 0 < 8
⊢ 0 ≠ 5 ∧ 0 ≠ 7 ↔ 0 = 1 ∨ 0 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «1»
m : ℕ
h₁✝ : 1 % 2 = 1
h₂✝ : 1 < 8
⊢ 1 ≠ 5 ∧ 1 ≠ 7 ↔ 1 = 1 ∨ 1 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «2»
m : ℕ
h₁✝ : 2 % 2 = 1
h₂✝ : 2 < 8
⊢ 2 ≠ 5 ∧ 2 ≠ 7 ↔ 2 = 1 ∨ 2 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «3»
m : ℕ
h₁✝ : 3 % 2 = 1
h₂✝ : 3 < 8
⊢ 3 ≠ 5 ∧ 3 ≠ 7 ↔ 3 = 1 ∨ 3 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «4»
m : ℕ
h₁✝ : 4 % 2 = 1
h₂✝ : 4 < 8
⊢ 4 ≠ 5 ∧ 4 ≠ 7 ↔ 4 = 1 ∨ 4 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «5»
m : ℕ
h₁✝ : 5 % 2 = 1
h₂✝ : 5 < 8
⊢ 5 ≠ 5 ∧ 5 ≠ 7 ↔ 5 = 1 ∨ 5 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «6»
m : ℕ
h₁✝ : 6 % 2 = 1
h₂✝ : 6 < 8
⊢ 6 ≠ 5 ∧ 6 ≠ 7 ↔ 6 = 1 ∨ 6 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «7»
m : ℕ
h₁✝ : 7 % 2 = 1
h₂✝ : 7 < 8
⊢ 7 ≠ 5 ∧ 7 ≠ 7 ↔ 7 = 1 ∨ 7 = 3
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
have hp₁ := (Prime.eq_two_or_odd <| @Fact.out p.Prime _).resolve_left hp
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
have hq₁ := (Prime.eq_two_or_odd <| @Fact.out q.Prime _).resolve_left hq
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
have hq₂ : ringChar (ZMod q) ≠ 2 := (ringChar_zmod_n q).substr hq
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
have h := quadraticChar_odd_prime ((ringChar_zmod_n p).substr hp) hq ((ringChar_zmod_n p).substr hpq)
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h :
  ↑(quadraticChar (ZMod p)) ↑q = ↑(quadraticChar (ZMod q)) (↑(↑χ₄ ↑(Fintype.card (ZMod p))) * ↑(Fintype.card (ZMod p)))
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
rw [card p] at h
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h : ↑(quadraticChar (ZMod p)) ↑q = ↑(quadraticChar (ZMod q)) (↑(↑χ₄ ↑p) * ↑p)
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
have nc : ∀ n r : ℕ, ((n : ℤ) : ZMod r) = n := fun n r => by norm_cast
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h : ↑(quadraticChar (ZMod p)) ↑q = ↑(quadraticChar (ZMod q)) (↑(↑χ₄ ↑p) * ↑p)
n r : ℕ
⊢ ↑↑n = ↑n
[PROOFSTEP]
norm_cast
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h : ↑(quadraticChar (ZMod p)) ↑q = ↑(quadraticChar (ZMod q)) (↑(↑χ₄ ↑p) * ↑p)
nc : ∀ (n r : ℕ), ↑↑n = ↑n
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
have nc' : (((-1) ^ (p / 2) : ℤ) : ZMod q) = (-1) ^ (p / 2) := by norm_cast
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h : ↑(quadraticChar (ZMod p)) ↑q = ↑(quadraticChar (ZMod q)) (↑(↑χ₄ ↑p) * ↑p)
nc : ∀ (n r : ℕ), ↑↑n = ↑n
⊢ ↑((-1) ^ (p / 2)) = (-1) ^ (p / 2)
[PROOFSTEP]
norm_cast
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
hpq : p ≠ q
hp₁ : p % 2 = 1
hq₁ : q % 2 = 1
hq₂ : ringChar (ZMod q) ≠ 2
h : ↑(quadraticChar (ZMod p)) ↑q = ↑(quadraticChar (ZMod q)) (↑(↑χ₄ ↑p) * ↑p)
nc : ∀ (n r : ℕ), ↑↑n = ↑n
nc' : ↑((-1) ^ (p / 2)) = (-1) ^ (p / 2)
⊢ legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
[PROOFSTEP]
rw [legendreSym, legendreSym, nc, nc, h, map_mul, mul_rotate', mul_comm (p / 2), ← pow_two,
  quadraticChar_sq_one (prime_ne_zero q p hpq.symm), mul_one, pow_mul, χ₄_eq_neg_one_pow hp₁, nc', map_pow,
  quadraticChar_neg_one hq₂, card q, χ₄_eq_neg_one_pow hq₁]
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
[PROOFSTEP]
cases' eq_or_ne p q with h h
[GOAL]
case inl
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p = q
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
[PROOFSTEP]
subst p
[GOAL]
case inl
q : ℕ
inst✝¹ : Fact (Nat.Prime q)
hq : q ≠ 2
inst✝ : Fact (Nat.Prime q)
hp : q ≠ 2
⊢ legendreSym q ↑q = (-1) ^ (q / 2 * (q / 2)) * legendreSym q ↑q
[PROOFSTEP]
rw [(eq_zero_iff q q).mpr (by exact_mod_cast nat_cast_self q), mul_zero]
[GOAL]
q : ℕ
inst✝¹ : Fact (Nat.Prime q)
hq : q ≠ 2
inst✝ : Fact (Nat.Prime q)
hp : q ≠ 2
⊢ ↑↑q = 0
[PROOFSTEP]
exact_mod_cast nat_cast_self q
[GOAL]
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
[PROOFSTEP]
have qr := congr_arg (· * legendreSym p q) (quadratic_reciprocity hp hq h)
[GOAL]
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
qr :
  (fun x => x * legendreSym p ↑q) (legendreSym q ↑p * legendreSym p ↑q) =
    (fun x => x * legendreSym p ↑q) ((-1) ^ (p / 2 * (q / 2)))
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
[PROOFSTEP]
have : ((q : ℤ) : ZMod p) ≠ 0 := by exact_mod_cast prime_ne_zero p q h
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
qr :
  (fun x => x * legendreSym p ↑q) (legendreSym q ↑p * legendreSym p ↑q) =
    (fun x => x * legendreSym p ↑q) ((-1) ^ (p / 2 * (q / 2)))
⊢ ↑↑q ≠ 0
[PROOFSTEP]
exact_mod_cast prime_ne_zero p q h
[GOAL]
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
qr :
  (fun x => x * legendreSym p ↑q) (legendreSym q ↑p * legendreSym p ↑q) =
    (fun x => x * legendreSym p ↑q) ((-1) ^ (p / 2 * (q / 2)))
this : ↑↑q ≠ 0
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
[PROOFSTEP]
simpa only [mul_assoc, ← pow_two, sq_one p this, mul_one] using qr
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 1
hq : q ≠ 2
⊢ legendreSym q ↑p = legendreSym p ↑q
[PROOFSTEP]
rw [quadratic_reciprocity' (Prime.mod_two_eq_one_iff_ne_two.mp (odd_of_mod_four_eq_one hp)) hq, pow_mul,
  neg_one_pow_div_two_of_one_mod_four hp, one_pow, one_mul]
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
⊢ legendreSym q ↑p = -legendreSym p ↑q
[PROOFSTEP]
let nop := @neg_one_pow_div_two_of_three_mod_four
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ legendreSym q ↑p = -legendreSym p ↑q
[PROOFSTEP]
rw [quadratic_reciprocity', pow_mul, nop hp, nop hq, neg_one_mul]
[GOAL]
case hp
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ p ≠ 2
[PROOFSTEP]
rwa [← Prime.mod_two_eq_one_iff_ne_two, odd_of_mod_four_eq_three]
[GOAL]
case hq
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ q ≠ 2
[PROOFSTEP]
rwa [← Prime.mod_two_eq_one_iff_ne_two, odd_of_mod_four_eq_three]
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
⊢ IsSquare ↑q ↔ IsSquare ↑p
[PROOFSTEP]
cases' eq_or_ne p q with h h
[GOAL]
case inl
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p = q
⊢ IsSquare ↑q ↔ IsSquare ↑p
[PROOFSTEP]
subst p
[GOAL]
case inl
q : ℕ
inst✝¹ : Fact (Nat.Prime q)
hq1 : q ≠ 2
inst✝ : Fact (Nat.Prime q)
hp1 : q % 4 = 1
⊢ IsSquare ↑q ↔ IsSquare ↑q
[PROOFSTEP]
rfl
[GOAL]
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p ≠ q
⊢ IsSquare ↑q ↔ IsSquare ↑p
[PROOFSTEP]
rw [← eq_one_iff' p (prime_ne_zero p q h), ← eq_one_iff' q (prime_ne_zero q p h.symm),
  quadratic_reciprocity_one_mod_four hp1 hq1]
[GOAL]
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp3 : p % 4 = 3
hq3 : q % 4 = 3
hpq : p ≠ q
⊢ IsSquare ↑q ↔ ¬IsSquare ↑p
[PROOFSTEP]
rw [← eq_one_iff' p (prime_ne_zero p q hpq), ← eq_neg_one_iff' q, quadratic_reciprocity_three_mod_four hp3 hq3, neg_inj]