MixedCharacteristicQp.lean

abbrev mrangeValueGroup (F : LocalField.{u, v} K) : Type v

abbrev ratSubfield (_F : LocalField.{u, v} K) [CharZero K] : Subfield K

theorem ratSubfield_eq_bot (F : LocalField.{u, v} K) [CharZero K] :
    F.ratSubfield = (⊥ : Subfield K)

theorem ratCast_mem_ratSubfield
    (F : LocalField.{u, v} K) [CharZero K] (q : ℚ) :
    (q : K) ∈ F.ratSubfield

def qpadicClosureSubfield
    (F : LocalField.{u, v} K) [CharZero K] : Subfield K

theorem qpadicClosureSubfield_coe
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    (F.qpadicClosureSubfield : Set K) =
      closure (F.ratSubfield : Set K) := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  rfl

theorem ratSubfield_le_qpadicClosureSubfield
    (F : LocalField.{u, v} K) [CharZero K] :
    F.ratSubfield ≤ F.qpadicClosureSubfield

theorem ratCast_mem_qpadicClosureSubfield
    (F : LocalField.{u, v} K) [CharZero K] (q : ℚ) :
    (q : K) ∈ F.qpadicClosureSubfield

theorem qpadicClosureSubfield_isClosed
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    IsClosed (F.qpadicClosureSubfield : Set K) := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  simpa [qpadicClosureSubfield] using
    (Subfield.isClosed_topologicalClosure F.ratSubfield)

theorem ratSubfield_denseRange_in_qpadicClosureSubfield
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    DenseRange
      (Set.inclusion
        (show (F.ratSubfield : Set K) ⊆
          (F.qpadicClosureSubfield : Set K) from
          F.ratSubfield_le_qpadicClosureSubfield)) := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  refine (denseRange_inclusion_iff
    (show (F.ratSubfield : Set K) ⊆
      (F.qpadicClosureSubfield : Set K) from
      F.ratSubfield_le_qpadicClosureSubfield)).2 ?_
  intro x hx
  exact hx

theorem qpadicClosureSubfield_le_of_ratSubfield_le
    (F : LocalField.{u, v} K) [CharZero K] {E : Subfield K}
    (hEclosed :
      letI : Valued K F.mrangeValueGroup :=
        mrangeRestrictValued F.toCompleteDVF
      IsClosed (E : Set K))
    (hRat : F.ratSubfield ≤ E) :
    F.qpadicClosureSubfield ≤ E := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  simpa [qpadicClosureSubfield] using
    (Subfield.topologicalClosure_minimal F.ratSubfield hRat hEclosed)

theorem qpadicClosureSubfield_completeSpace
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    letI : NontriviallyNormedField K :=
      mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
    CompleteSpace F.qpadicClosureSubfield := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  let : NontriviallyNormedField K :=
    mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  have : CompleteSpace K :=
    F.mrangeRestrict_completeSpace
  exact
    (F.qpadicClosureSubfield_isClosed).completeSpace_coe

def ratCastToQpadicClosureSubfield
    (F : LocalField.{u, v} K) [CharZero K] :
    ℚ →+* F.qpadicClosureSubfield

theorem ratCastToQpadicClosureSubfield_apply
    (F : LocalField.{u, v} K) [CharZero K] (q : ℚ) :
    ((F.ratCastToQpadicClosureSubfield q :
      F.qpadicClosureSubfield) : K) = q

def ratCastWithValToQpadicClosureSubfield
    (F : LocalField.{u, v} K) [CharZero K] :
    WithVal (Rat.padicValuation F.residueCharacteristic) →+*
      F.qpadicClosureSubfield

theorem ratCastWithValToQpadicClosureSubfield_apply
    (F : LocalField.{u, v} K) [CharZero K]
    (q : WithVal (Rat.padicValuation F.residueCharacteristic)) :
    ((F.ratCastWithValToQpadicClosureSubfield q :
      F.qpadicClosureSubfield) : K) =
      ((WithVal.equiv
        (Rat.padicValuation F.residueCharacteristic) q : ℚ) : K)

theorem mrangeRestrict_valuation_ratCast_le_one_iff_padicValuation_le_one
    (F : LocalField.{u, v} K) [CharZero K] (q : ℚ) :
    _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict
        F.toCompleteDVF (q : K) ≤ 1 ↔
      Rat.padicValuation F.residueCharacteristic q ≤ 1

theorem ratCast_preimage_mrangeRestrict_valuationSubring_eq_padicValuationSubring
    (F : LocalField.{u, v} K) [CharZero K] :
    (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict
        F.toCompleteDVF).valuationSubring.comap (Rat.castHom K) =
      (Rat.padicValuation F.residueCharacteristic).valuationSubring

theorem ratCast_mrangeRestrict_valuation_isEquiv_padicValuation
    (F : LocalField.{u, v} K) [CharZero K] :
    ((_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict
        F.toCompleteDVF).comap (Rat.castHom K)).IsEquiv
      (Rat.padicValuation F.residueCharacteristic)

theorem mrangeRestrict_exists_residueCharacteristic_pow_lt_unit
    (F : LocalField.{u, v} K) [CharZero K]
    (gamma : F.mrangeValueGroupˣ) :
    ∃ N : ℕ,
      _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict F.toCompleteDVF
        (((F.residueCharacteristic ^ N : ℕ) : K)) < gamma

theorem ratCastWithValToK_uniformContinuous
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    UniformContinuous
      ((Rat.castHom K).comp
        (WithVal.equiv
          (Rat.padicValuation F.residueCharacteristic)).toRingHom) := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  let f : WithVal (Rat.padicValuation F.residueCharacteristic) → K :=
    ((Rat.castHom K).comp
      (WithVal.equiv
        (Rat.padicValuation F.residueCharacteristic)).toRingHom)
  let vq := Rat.padicValuation F.residueCharacteristic
  let vWith : _root_.Valuation (WithVal vq) ℤᵐ⁰ := Valued.v
  let w : _root_.Valuation K F.mrangeValueGroup :=
    _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict
      F.toCompleteDVF
  change UniformContinuous f
  refine
    ((Valued.hasBasis_uniformity
        (WithVal (Rat.padicValuation F.residueCharacteristic))
        ℤᵐ⁰).uniformContinuous_iff
        (Valued.hasBasis_uniformity K F.mrangeValueGroup)).2 ?_
  intro gamma _
  let gamma' : F.mrangeValueGroupˣ :=
    Units.map
      MonoidWithZeroHom.ValueGroup₀.embedding.toMonoidHom gamma
  obtain ⟨N, hN⟩ :=
    F.mrangeRestrict_exists_residueCharacteristic_pow_lt_unit gamma'
  let pNQ : ℚ := ((F.residueCharacteristic ^ N : ℕ) : ℚ)
  have hpN_nat_ne : F.residueCharacteristic ^ N ≠ 0 :=
    pow_ne_zero N F.residueCharacteristic_ne_zero
  have hpNQ_ne : pNQ ≠ 0 := by
    simpa [pNQ] using
      (Nat.cast_ne_zero.mpr hpN_nat_ne :
        ((F.residueCharacteristic ^ N : ℕ) : ℚ) ≠ 0)
  let pNW : WithVal vq := (WithVal.equiv vq).symm pNQ
  have hpNW_ne : vWith pNW ≠ 0 := by
    change vq pNQ ≠ 0
    exact (vq.pos_iff.2 hpNQ_ne).ne'
  have hpNW_restrict_ne : vWith.restrict pNW ≠ 0 := by
    simpa using hpNW_ne
  let delta :
      (MonoidWithZeroHom.ValueGroup₀ (.ofClass vWith))ˣ :=
    Units.mk0 (vWith.restrict pNW) hpNW_restrict_ne
  refine ⟨delta, trivial, ?_⟩
  intro x y hxy
  let xq : ℚ :=
    WithVal.equiv (Rat.padicValuation F.residueCharacteristic) x
  let yq : ℚ :=
    WithVal.equiv (Rat.padicValuation F.residueCharacteristic) y
  have hpadic :
      Rat.padicValuation F.residueCharacteristic (yq - xq) <
        Rat.padicValuation F.residueCharacteristic pNQ := by
    change vq (yq - xq) < vq pNQ
    change vWith.restrict (y - x) < vWith.restrict pNW at hxy
    have hvWith : vWith (y - x) < vWith pNW :=
      (_root_.Valuation.restrict_lt_iff vWith).1 hxy
    change vq (yq - xq) < vq pNQ at hvWith
    exact hvWith
  have hcomap :
      _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict
          F.toCompleteDVF ((yq - xq : ℚ) : K) <
        _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict
            F.toCompleteDVF ((pNQ : ℚ) : K) := by
    have hEquiv :=
      F.ratCast_mrangeRestrict_valuation_isEquiv_padicValuation
    have hlt :=
      (hEquiv.lt_iff_lt (x := yq - xq) (y := pNQ)).2 hpadic
    simpa [pNQ] using hlt
  have hfsub :
      f y - f x = ((yq - xq : ℚ) : K) := by
    simp [f, xq, yq]
  change (Valued.v : _root_.Valuation K F.mrangeValueGroup).restrict (f y - f x) < gamma
  rw [_root_.Valuation.restrict_lt_iff_lt_embedding]
  change w (f y - f x) < (gamma' : F.mrangeValueGroup)
  calc
    w (f y - f x) = w ((yq - xq : ℚ) : K) := by
          rw [hfsub]
    _ < w ((pNQ : ℚ) : K) := hcomap
    _ = w (((F.residueCharacteristic ^ N : ℕ) : K)) := by
          congr 1
          simp [pNQ]
    _ < gamma' := hN

theorem ratCastWithValToK_isUniformInducing
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    IsUniformInducing
      ((Rat.castHom K).comp
        (WithVal.equiv
          (Rat.padicValuation F.residueCharacteristic)).toRingHom) := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  let f : WithVal (Rat.padicValuation F.residueCharacteristic) → K :=
    ((Rat.castHom K).comp
      (WithVal.equiv
        (Rat.padicValuation F.residueCharacteristic)).toRingHom)
  let vq := Rat.padicValuation F.residueCharacteristic
  let vWith : _root_.Valuation (WithVal vq) ℤᵐ⁰ := Valued.v
  let w : _root_.Valuation K F.mrangeValueGroup :=
    _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict
      F.toCompleteDVF
  change IsUniformInducing f
  refine
    ((Valued.hasBasis_uniformity
        (WithVal (Rat.padicValuation F.residueCharacteristic))
        ℤᵐ⁰).isUniformInducing_iff
        (Valued.hasBasis_uniformity K F.mrangeValueGroup)).2 ?_
  constructor
  · exact
      ((Valued.hasBasis_uniformity
          (WithVal (Rat.padicValuation F.residueCharacteristic))
          ℤᵐ⁰).uniformContinuous_iff
          (Valued.hasBasis_uniformity K F.mrangeValueGroup)).1
        F.ratCastWithValToK_uniformContinuous
  · intro delta _
    obtain ⟨q, hq⟩ :=
      Rat.surjective_padicValuation F.residueCharacteristic
        (MonoidWithZeroHom.ValueGroup₀.embedding
          (f := vWith.toMonoidWithZeroHom) delta.1)
    have hq_ne : q ≠ 0 := by
      intro hzero
      have hdelta_zero :
          MonoidWithZeroHom.ValueGroup₀.embedding
              (f := vWith.toMonoidWithZeroHom) delta.1 = 0 := by
        simpa [hzero] using hq.symm
      exact
        (MonoidWithZeroHom.ValueGroup₀.embedding_unit_ne_zero delta)
          hdelta_zero
    have hqK_ne : ((q : ℚ) : K) ≠ 0 := by
      exact Rat.cast_ne_zero.mpr hq_ne
    have hvalue_ne :
        _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict
            F.toCompleteDVF ((q : ℚ) : K) ≠ 0 := by
      rw [← Subtype.coe_ne_coe]
      simpa [_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict_apply] using
        ((F.toCompleteDVF.valuation.pos_iff).2 hqK_ne).ne'
    have hrestrict_ne : w.restrict ((q : ℚ) : K) ≠ 0 := by
      simpa using hvalue_ne
    let gamma :
        (MonoidWithZeroHom.ValueGroup₀ (.ofClass w))ˣ :=
      Units.mk0 (w.restrict ((q : ℚ) : K)) hrestrict_ne
    refine ⟨gamma, trivial, ?_⟩
    intro x y hxy
    let xq : ℚ :=
      WithVal.equiv (Rat.padicValuation F.residueCharacteristic) x
    let yq : ℚ :=
      WithVal.equiv (Rat.padicValuation F.residueCharacteristic) y
    have hfsub :
        f y - f x = ((yq - xq : ℚ) : K) := by
      simp [f, xq, yq]
    have hcomap :
        _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict
            F.toCompleteDVF ((yq - xq : ℚ) : K) <
          _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict
              F.toCompleteDVF ((q : ℚ) : K) := by
      change w.restrict (f y - f x) < w.restrict ((q : ℚ) : K) at hxy
      rw [hfsub] at hxy
      exact (_root_.Valuation.restrict_lt_iff w).1 hxy
    have hpadic :
        Rat.padicValuation F.residueCharacteristic (yq - xq) <
          Rat.padicValuation F.residueCharacteristic q := by
      have hEquiv :=
        F.ratCast_mrangeRestrict_valuation_isEquiv_padicValuation
      exact (hEquiv.lt_iff_lt (x := yq - xq) (y := q)).1 hcomap
    change vWith.restrict (y - x) < delta
    rw [_root_.Valuation.restrict_lt_iff_lt_embedding]
    change
      vq (yq - xq) <
        MonoidWithZeroHom.ValueGroup₀.embedding
          (f := vWith.toMonoidWithZeroHom) delta.1
    simpa [hq] using hpadic

theorem ratCastWithValToQpadicClosureSubfield_uniformContinuous
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    UniformContinuous F.ratCastWithValToQpadicClosureSubfield := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  exact
    F.ratCastWithValToK_uniformContinuous.subtype_mk
      (fun q => F.ratCast_mem_qpadicClosureSubfield
        ((WithVal.equiv
          (Rat.padicValuation F.residueCharacteristic) q : ℚ)))

theorem ratCastWithValToQpadicClosureSubfield_isUniformInducing
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    IsUniformInducing F.ratCastWithValToQpadicClosureSubfield := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  have hK :
      IsUniformInducing
        (((↑) : F.qpadicClosureSubfield → K) ∘
          F.ratCastWithValToQpadicClosureSubfield) := by
    simpa [Function.comp_def, ratCastWithValToQpadicClosureSubfield,
      ratCastToQpadicClosureSubfield] using
      F.ratCastWithValToK_isUniformInducing
  exact
    (isUniformInducing_val
      (F.qpadicClosureSubfield : Set K)).of_comp_iff.1 hK

theorem ratCastWithValToQpadicClosureSubfield_denseRange
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    DenseRange F.ratCastWithValToQpadicClosureSubfield := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  let i : ↥(F.ratSubfield : Set K) → F.qpadicClosureSubfield :=
    Set.inclusion
      (show (F.ratSubfield : Set K) ⊆
        (F.qpadicClosureSubfield : Set K) from
        F.ratSubfield_le_qpadicClosureSubfield)
  let j : WithVal (Rat.padicValuation F.residueCharacteristic) →
      ↥(F.ratSubfield : Set K) :=
    fun q =>
      ⟨((WithVal.equiv
        (Rat.padicValuation F.residueCharacteristic) q : ℚ) : K),
        F.ratCast_mem_ratSubfield
          ((WithVal.equiv
            (Rat.padicValuation F.residueCharacteristic) q : ℚ))⟩
  have hi : DenseRange i := by
    simpa only [i] using
      F.ratSubfield_denseRange_in_qpadicClosureSubfield
  have hj : Function.Surjective j := by
    intro z
    rcases z.2 with ⟨q, hq⟩
    refine ⟨(WithVal.equiv
      (Rat.padicValuation F.residueCharacteristic)).symm q, ?_⟩
    ext
    simpa [j, ratSubfield] using hq
  have hcomp : DenseRange (i ∘ j) :=
    hi.comp hj.denseRange (continuous_inclusion _)
  have hfun : i ∘ j = F.ratCastWithValToQpadicClosureSubfield := by
    funext q
    apply Subtype.ext
    rfl
  rw [hfun] at hcomp
  exact hcomp

theorem ratCastToQpadicClosureSubfield_denseRange
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    DenseRange F.ratCastToQpadicClosureSubfield := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  apply DenseRange.of_comp
    (g := WithVal.equiv
      (Rat.padicValuation F.residueCharacteristic))
  simpa [Function.comp_def, ratCastWithValToQpadicClosureSubfield]
    using F.ratCastWithValToQpadicClosureSubfield_denseRange

def qpadicCompletionToQpadicClosureSubfield
    (F : LocalField.{u, v} K) [CharZero K] :
    (Rat.padicValuation F.residueCharacteristic).Completion →+*
      F.qpadicClosureSubfield

theorem qpadicCompletionToQpadicClosureSubfield_coe
    (F : LocalField.{u, v} K) [CharZero K]
    (q : WithVal (Rat.padicValuation F.residueCharacteristic)) :
    F.qpadicCompletionToQpadicClosureSubfield q =
      F.ratCastWithValToQpadicClosureSubfield q

theorem qpadicCompletionToQpadicClosureSubfield_isUniformInducing
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    letI : NontriviallyNormedField K :=
      mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
    IsUniformInducing F.qpadicCompletionToQpadicClosureSubfield := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  let : NontriviallyNormedField K :=
    mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  have : CompleteSpace F.qpadicClosureSubfield :=
    F.qpadicClosureSubfield_completeSpace
  simpa [qpadicCompletionToQpadicClosureSubfield,
    UniformSpace.Completion.extensionHom] using
    UniformSpace.Completion.isUniformInducing_extension
      (f := F.ratCastWithValToQpadicClosureSubfield)
      F.ratCastWithValToQpadicClosureSubfield_isUniformInducing

theorem qpadicCompletionToQpadicClosureSubfield_denseRange
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    letI : NontriviallyNormedField K :=
      mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
    DenseRange F.qpadicCompletionToQpadicClosureSubfield := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  let : NontriviallyNormedField K :=
    mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  apply DenseRange.of_comp
    (g := fun q : WithVal (Rat.padicValuation F.residueCharacteristic) =>
      (q : (Rat.padicValuation F.residueCharacteristic).Completion))
  simpa [Function.comp_def,
    F.qpadicCompletionToQpadicClosureSubfield_coe] using
    F.ratCastWithValToQpadicClosureSubfield_denseRange

def qpadicNumbersToQpadicClosureSubfield
    (F : LocalField.{u, v} K) [CharZero K] :
    ℚ_[F.residueCharacteristic] →+* F.qpadicClosureSubfield

theorem qpadicNumbersToQpadicClosureSubfield_ratCast
    (F : LocalField.{u, v} K) [CharZero K] (q : ℚ) :
    F.qpadicNumbersToQpadicClosureSubfield
        (q : ℚ_[F.residueCharacteristic]) =
      F.ratCastToQpadicClosureSubfield q

theorem qpadicNumbersToQpadicClosureSubfield_isUniformInducing
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    letI : NontriviallyNormedField K :=
      mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
    IsUniformInducing F.qpadicNumbersToQpadicClosureSubfield := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  let : NontriviallyNormedField K :=
    mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  have hcomp :
      IsUniformInducing
        (F.qpadicCompletionToQpadicClosureSubfield ∘
          (Padic.withValUniformEquiv
            (p := F.residueCharacteristic)).symm) :=
    F.qpadicCompletionToQpadicClosureSubfield_isUniformInducing.comp
      (Padic.withValUniformEquiv
        (p := F.residueCharacteristic)).symm.isUniformInducing
  have hinv :
      ⇑(Padic.withValUniformEquiv
          (p := F.residueCharacteristic)).symm =
        ⇑(Padic.withValRingEquiv
          (p := F.residueCharacteristic)).symm := by
    funext x
    exact congrArg
      (fun e :
          (Rat.padicValuation F.residueCharacteristic).Completion ≃
            ℚ_[F.residueCharacteristic] => e.symm x)
      Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv
  change
    IsUniformInducing
      (F.qpadicCompletionToQpadicClosureSubfield ∘
        ⇑(Padic.withValRingEquiv
          (p := F.residueCharacteristic)).symm)
  rw [← hinv]
  exact hcomp

theorem qpadicNumbersToQpadicClosureSubfield_isClosed_range
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    letI : NontriviallyNormedField K :=
      mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
    IsClosed (Set.range F.qpadicNumbersToQpadicClosureSubfield) := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  let : NontriviallyNormedField K :=
    mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  have hEmbedding :
      IsUniformEmbedding F.qpadicNumbersToQpadicClosureSubfield :=
    ⟨F.qpadicNumbersToQpadicClosureSubfield_isUniformInducing,
      RingHom.injective _⟩
  exact hEmbedding.isClosedEmbedding.isClosed_range

theorem qpadicNumbersToQpadicClosureSubfield_denseRange
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    letI : NontriviallyNormedField K :=
      mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
    DenseRange F.qpadicNumbersToQpadicClosureSubfield := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  let : NontriviallyNormedField K :=
    mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  apply DenseRange.of_comp
    (g := ((↑) : ℚ → ℚ_[F.residueCharacteristic]))
  have hfun :
      F.qpadicNumbersToQpadicClosureSubfield ∘
          ((↑) : ℚ → ℚ_[F.residueCharacteristic]) =
        F.ratCastToQpadicClosureSubfield := by
    funext q
    exact F.qpadicNumbersToQpadicClosureSubfield_ratCast q
  rw [hfun]
  exact F.ratCastToQpadicClosureSubfield_denseRange

theorem qpadicNumbersToQpadicClosureSubfield_surjective
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    letI : NontriviallyNormedField K :=
      mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
    Function.Surjective F.qpadicNumbersToQpadicClosureSubfield := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  let : NontriviallyNormedField K :=
    mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  rw [← Set.range_eq_univ]
  have hdense := F.qpadicNumbersToQpadicClosureSubfield_denseRange
  have hclosed := F.qpadicNumbersToQpadicClosureSubfield_isClosed_range
  exact hclosed.closure_eq.symm.trans hdense.closure_range

def qpadicNumbersEquivQpadicClosureSubfield
    (F : LocalField.{u, v} K) [CharZero K] :
    ℚ_[F.residueCharacteristic] ≃+* F.qpadicClosureSubfield

theorem qpadicNumbersEquivQpadicClosureSubfield_apply
    (F : LocalField.{u, v} K) [CharZero K]
    (x : ℚ_[F.residueCharacteristic]) :
    F.qpadicNumbersEquivQpadicClosureSubfield x =
      F.qpadicNumbersToQpadicClosureSubfield x

theorem qpadicNumbersEquivQpadicClosureSubfield_ratCast
    (F : LocalField.{u, v} K) [CharZero K] (q : ℚ) :
    F.qpadicNumbersEquivQpadicClosureSubfield
        (q : ℚ_[F.residueCharacteristic]) =
      F.ratCastToQpadicClosureSubfield q

def qpadicClosureSubfield_nontriviallyNormedField
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    letI : NontriviallyNormedField K :=
      mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
    NontriviallyNormedField F.qpadicClosureSubfield := by
  letI : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  haveI :
      (Valued.v : _root_.Valuation K F.mrangeValueGroup).RankOne := by
    change
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict
        F.toCompleteDVF).RankOne
    exact
      _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict_rankOne
        F.toCompleteDVF
  letI : NontriviallyNormedField K :=
    mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  let pSub : F.qpadicClosureSubfield :=
    F.ratCastToQpadicClosureSubfield (F.residueCharacteristic : ℚ)
  have hpSub_coe :
      (pSub : K) = (F.residueCharacteristic : K) := by
    simp [pSub]
  refine NontriviallyNormedField.ofNormNeOne ?_
  refine ⟨pSub, ?_, ?_⟩
  · intro hp
    have hpK : (pSub : K) = 0 := by
      simpa using congrArg Subtype.val hp
    rw [hpSub_coe] at hpK
    exact F.natCast_residueCharacteristic_ne_zero_of_charZero hpK
  · have hpVal_lt_one :
        _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict F.toCompleteDVF
          (F.residueCharacteristic : K) < 1 := by
      rw [← Subtype.coe_lt_coe]
      simpa [_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict_apply] using
        F.valuation_natCast_residueCharacteristic_lt_one
    have hpNorm_lt_one_K :
        ‖(F.residueCharacteristic : K)‖ < 1 := by
      simpa [mrangeRestrictValued] using
        (Valued.toNormedField.norm_lt_one_iff
          (x := (F.residueCharacteristic : K))).2 hpVal_lt_one
    have hpNorm_lt_one : ‖pSub‖ < 1 := by
      change ‖(pSub : K)‖ < 1
      simpa [hpSub_coe] using hpNorm_lt_one_K
    exact ne_of_lt hpNorm_lt_one

def qpadicClosureSubfield_normedAlgebra
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    letI : NontriviallyNormedField K :=
      mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
    letI : NontriviallyNormedField F.qpadicClosureSubfield :=
      F.qpadicClosureSubfield_nontriviallyNormedField
    NormedAlgebra F.qpadicClosureSubfield K := by
  letI : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  letI : NontriviallyNormedField K :=
    mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  letI : NontriviallyNormedField F.qpadicClosureSubfield :=
    F.qpadicClosureSubfield_nontriviallyNormedField
  exact
    { (inferInstance : Algebra F.qpadicClosureSubfield K) with
      norm_smul_le := fun a x => by
        change ‖(a : K) * x‖ ≤ ‖(a : K)‖ * ‖x‖
        exact norm_mul_le (a : K) x }

theorem finiteDimensional_over_qpadicClosureSubfield
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Valued K F.mrangeValueGroup :=
      mrangeRestrictValued F.toCompleteDVF
    letI : NontriviallyNormedField K :=
      mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
    letI : NontriviallyNormedField F.qpadicClosureSubfield :=
      F.qpadicClosureSubfield_nontriviallyNormedField
    letI : NormedAlgebra F.qpadicClosureSubfield K :=
      F.qpadicClosureSubfield_normedAlgebra
    FiniteDimensional F.qpadicClosureSubfield K := by
  let : Valued K F.mrangeValueGroup :=
    mrangeRestrictValued F.toCompleteDVF
  let : NontriviallyNormedField K :=
    mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  let : NontriviallyNormedField F.qpadicClosureSubfield :=
    F.qpadicClosureSubfield_nontriviallyNormedField
  let : NormedAlgebra F.qpadicClosureSubfield K :=
    F.qpadicClosureSubfield_normedAlgebra
  have : ProperSpace K :=
    F.mrangeRestrict_properSpace
  have : CompleteSpace F.qpadicClosureSubfield :=
    (F.qpadicClosureSubfield_isClosed : IsClosed
      (F.qpadicClosureSubfield : Set K)).completeSpace_coe
  exact
    FiniteDimensional.of_locallyCompactSpace F.qpadicClosureSubfield

def qpadicNumbersAlgebra
    (F : LocalField.{u, v} K) [CharZero K] :
    Algebra ℚ_[F.residueCharacteristic] K

theorem qpadicNumbersAlgebra_algebraMap
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Algebra ℚ_[F.residueCharacteristic] K :=
      F.qpadicNumbersAlgebra
    algebraMap ℚ_[F.residueCharacteristic] K =
      F.qpadicClosureSubfield.subtype.comp
        (F.qpadicNumbersEquivQpadicClosureSubfield :
          ℚ_[F.residueCharacteristic] →+* F.qpadicClosureSubfield) := by
  rfl

theorem qpadicNumbersAlgebra_algebraMap_apply
    (F : LocalField.{u, v} K) [CharZero K]
    (x : ℚ_[F.residueCharacteristic]) :
    letI : Algebra ℚ_[F.residueCharacteristic] K :=
      F.qpadicNumbersAlgebra
    algebraMap ℚ_[F.residueCharacteristic] K x =
      (F.qpadicNumbersEquivQpadicClosureSubfield x : K) := by
  rfl

theorem finiteDimensional_over_qpadicNumbers
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Algebra ℚ_[F.residueCharacteristic] K :=
      F.qpadicNumbersAlgebra
    FiniteDimensional ℚ_[F.residueCharacteristic] K := by
  let : Algebra ℚ_[F.residueCharacteristic] K :=
    F.qpadicNumbersAlgebra
  let : Valued K F.mrangeValueGroup :=
    _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F.toCompleteDVF
  let : NontriviallyNormedField K :=
    mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  let : NontriviallyNormedField F.qpadicClosureSubfield :=
    F.qpadicClosureSubfield_nontriviallyNormedField
  let : NormedAlgebra F.qpadicClosureSubfield K :=
    F.qpadicClosureSubfield_normedAlgebra
  have : FiniteDimensional F.qpadicClosureSubfield K :=
    F.finiteDimensional_over_qpadicClosureSubfield
  have hcompat :
      (algebraMap F.qpadicClosureSubfield K).comp
          (F.qpadicNumbersEquivQpadicClosureSubfield :
            ℚ_[F.residueCharacteristic] →+* F.qpadicClosureSubfield) =
        (RingEquiv.refl K).toRingHom.comp
          (algebraMap ℚ_[F.residueCharacteristic] K) := by
    ext x
    rfl
  have hrank :
      Module.rank ℚ_[F.residueCharacteristic] K =
        Module.rank F.qpadicClosureSubfield K := by
    simpa using
      (Algebra.rank_eq_of_equiv_equiv
        F.qpadicNumbersEquivQpadicClosureSubfield
        (RingEquiv.refl K) hcompat)
  exact
    FiniteDimensional.of_rank_eq_nat
      (n := Module.finrank F.qpadicClosureSubfield K) <| by
        simpa [Module.finrank_eq_rank'] using hrank

theorem mixedCharacteristic_exists_qpadic_finiteExtension
    (F : LocalField.{u, v} K) [CharZero K] :
    ∃ p : ℕ, p = F.residueCharacteristic ∧
      ∃ hp : Nat.Prime p,
        letI : Fact p.Prime := ⟨hp⟩
        ∃ hAlg : Algebra ℚ_[p] K,
          letI : Algebra ℚ_[p] K := hAlg
          FiniteDimensional ℚ_[p] K := by
  refine
    ⟨F.residueCharacteristic, rfl, F.residueCharacteristic_prime, ?_⟩
  exact
    ⟨F.qpadicNumbersAlgebra, F.finiteDimensional_over_qpadicNumbers⟩