import Mathlib
import Definitions.Def_AlgebraicCurve_DivisorClassGroup
import Definitions.Def_AlgebraicCurve_DivisorPushPull
import Definitions.Def_DedekindDomain_AdicValuation_InlineSpecific

set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 1600000

instance {K L : Type*} [Field K] [Semiring L] (O : ValuationSubring K) [Algebra K L] :
    Algebra O L where
  smul r x := r.1 • x
  algebraMap := (algebraMap K L).comp (algebraMap O K)
  commutes' _ _ := by simp [Algebra.commutes]
  smul_def' _ _ := by simp [← Algebra.smul_def]; rfl

set_option autoImplicit false

set_option synthInstance.maxHeartbeats 800000
set_option maxHeartbeats 1600000

noncomputable section

open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom

namespace AlgebraicCurve.Place

section AdicCompletion

variable {K F : Type*} [Field K] [Field F] [Algebra K F] (V : Place K F)

abbrev adicCompletion : Type _ := V.heightOneSpectrum.adicCompletion F

abbrev adicCompletionIntegers : ValuationSubring V.adicCompletion :=
  V.heightOneSpectrum.adicCompletionIntegers F

end AdicCompletion

section WithValLevel

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

theorem kw_ffgc_adicValuation_algebraMap (x : F) :
    W.adicValuation (algebraMap F F' x)
      = (W.restrict F).adicValuation x ^ W.ramificationIndex F := by
  rcases eq_or_ne x 0 with rfl | hx
  · simp [adicValuation, zero_pow (W.ramificationIndex_pos (F := F)).ne']
  · have hord := W.ord_restrict (F := F) x
    have hax : algebraMap F F' x ≠ 0 :=
      (map_ne_zero_iff _ (algebraMap F F').injective).mpr hx
    have hV0 : (W.restrict F).adicValuation x ≠ 0 := (W.restrict F).adicValuation_ne_zero hx
    have hW0 : W.adicValuation (algebraMap F F' x) ≠ 0 := W.adicValuation_ne_zero hax
    unfold ord at hord
    have hlog : WithZero.log (W.adicValuation (algebraMap F F' x))
        = WithZero.log ((W.restrict F).adicValuation x ^ W.ramificationIndex F) := by
      rw [← zpow_natCast, log_zpow, zsmul_eq_mul, Int.cast_natCast]; linarith
    rw [← exp_log hW0, hlog, exp_log (pow_ne_zero _ hV0)]

theorem kw_ffgc_valued_withValMapAlgebraMap
    (x : WithVal ((W.restrict F).heightOneSpectrum.valuation F)) :
    Valued.v (WithVal.map ((W.restrict F).heightOneSpectrum.valuation F)
      (W.heightOneSpectrum.valuation F') (algebraMap F F') x)
        = Valued.v x ^ W.ramificationIndex F := by
  rw [WithVal.map_apply, WithVal.valued_toVal]
  exact kw_ffgc_adicValuation_algebraMap F W x.ofVal

set_option backward.isDefEq.respectTransparency false in

theorem kw_ffgc_uniformContinuous_withValMapAlgebraMap :
    UniformContinuous (WithVal.map ((W.restrict F).heightOneSpectrum.valuation F)
      (W.heightOneSpectrum.valuation F') (algebraMap F F')) := by
  refine uniformContinuous_of_continuousAt_zero _ ?_
  simp_rw [ContinuousAt, map_zero, (Valued.hasBasis_nhds_zero _ _).tendsto_iff
    (Valued.hasBasis_nhds_zero _ _), true_and, forall_const]
  intro γ

  have hγ0 : (ValueGroup₀.embedding (γ.val) : ℤᵐ⁰) ≠ 0 :=
    (γ.isUnit.map ValueGroup₀.embedding).ne_zero
  have hc0 : min (ValueGroup₀.embedding γ.val) (1 : ℤᵐ⁰) ≠ 0 :=
    (lt_min (zero_lt_iff.mpr hγ0) zero_lt_one).ne'

  obtain ⟨x₀, hx₀⟩ :=
    (W.restrict F).heightOneSpectrum.valuation_surjective F
      (min (ValueGroup₀.embedding γ.val) 1)
  have hx₀v : Valued.v (WithVal.toVal ((W.restrict F).heightOneSpectrum.valuation F) x₀) =
      min (ValueGroup₀.embedding γ.val) 1 := by
    rw [WithVal.valued_toVal, hx₀]
  have hδ0 : Valued.v.restrict
      (WithVal.toVal ((W.restrict F).heightOneSpectrum.valuation F) x₀) ≠ 0 := by
    rw [ne_eq, Valuation.restrict_eq_zero_iff, hx₀v]
    exact hc0
  refine ⟨Units.mk0 _ hδ0, fun x hx => ?_⟩
  simp only [Set.mem_setOf_eq, Units.val_mk0] at hx ⊢
  rw [Valuation.restrict_lt_iff, hx₀v] at hx

  rw [Valuation.restrict_lt_iff_lt_embedding, kw_ffgc_valued_withValMapAlgebraMap F W x]

  calc Valued.v x ^ W.ramificationIndex F
      ≤ Valued.v x ^ 1 :=
        pow_le_pow_right_of_le_one' (hx.trans_le (min_le_right _ _)).le
          (W.ramificationIndex_pos (F := F))
    _ = Valued.v x := pow_one _
    _ < ValueGroup₀.embedding γ.val := hx.trans_le (min_le_left _ _)

end WithValLevel

section CompletionComap

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

def kw_ffgc_adicCompletionComap : (W.restrict F).adicCompletion →+* W.adicCompletion :=
  ((IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv F' W.heightOneSpectrum).symm.toRingHom.comp
    (UniformSpace.Completion.mapRingHom
      (WithVal.map ((W.restrict F).heightOneSpectrum.valuation F)
        (W.heightOneSpectrum.valuation F') (algebraMap F F'))
      (kw_ffgc_uniformContinuous_withValMapAlgebraMap F W).continuous)).comp
    (IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv F (W.restrict F).heightOneSpectrum).toRingHom

theorem kw_ffgc_continuous_adicCompletionComap :
    Continuous (kw_ffgc_adicCompletionComap F W) := by
  have h : ⇑(kw_ffgc_adicCompletionComap F W) =
      IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion ∘ UniformSpace.Completion.map
        (WithVal.map ((W.restrict F).heightOneSpectrum.valuation F)
          (W.heightOneSpectrum.valuation F') (algebraMap F F')) ∘
        IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion := rfl
  rw [h]
  exact (IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_ofCompletion F' _).comp
    (UniformSpace.Completion.continuous_map.comp
      (IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_toCompletion F _))

theorem kw_ffgc_adicCompletionComap_coe
    (x : WithVal ((W.restrict F).heightOneSpectrum.valuation F)) :
    kw_ffgc_adicCompletionComap F W (x : (W.restrict F).adicCompletion)
      = (WithVal.map ((W.restrict F).heightOneSpectrum.valuation F)
          (W.heightOneSpectrum.valuation F') (algebraMap F F') x : W.adicCompletion) :=
  by
  apply IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
  exact UniformSpace.Completion.mapRingHom_coe
    (kw_ffgc_uniformContinuous_withValMapAlgebraMap F W).continuous x

open WithZeroTopology in

theorem kw_ffgc_valued_adicCompletionComap (x : (W.restrict F).adicCompletion) :
    Valued.v (kw_ffgc_adicCompletionComap F W x)
      = Valued.v x ^ W.ramificationIndex F := by
  obtain ⟨x, rfl⟩ :=
    IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_surjective F _ x
  induction x using UniformSpace.Completion.induction_on with
  | hp =>
    refine isClosed_eq
      ((Valued.continuous_valuation_of_surjective
        (W.heightOneSpectrum.valuedAdicCompletion_surjective F')).comp
        ((kw_ffgc_continuous_adicCompletionComap F W).comp
          (IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_ofCompletion F _)))
      (((Valued.continuous_valuation_of_surjective
        ((W.restrict F).heightOneSpectrum.valuedAdicCompletion_surjective F)).comp
          (IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_ofCompletion F _)).pow _)
  | ih a =>
    rw [kw_ffgc_adicCompletionComap_coe]
    simp only [IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_ofCompletion,
      Valued.valuedCompletion_apply]
    exact kw_ffgc_valued_withValMapAlgebraMap F W a

end CompletionComap

end AlgebraicCurve.Place

set_option autoImplicit false

set_option synthInstance.maxHeartbeats 800000
set_option maxHeartbeats 1600000

noncomputable section

open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom

namespace AlgebraicCurve.Place

section IntegerComap

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

theorem kw_ffgc_adicCompletionComap_mem_integers
    {x : (W.restrict F).adicCompletion} (hx : x ∈ (W.restrict F).adicCompletionIntegers) :
    kw_ffgc_adicCompletionComap F W x ∈ W.adicCompletionIntegers := by
  rw [HeightOneSpectrum.mem_adicCompletionIntegers] at hx ⊢
  rw [kw_ffgc_valued_adicCompletionComap]
  exact pow_le_one' hx _

def kw_ffgc_adicCompletionComapIntegers :
    (W.restrict F).adicCompletionIntegers →+* W.adicCompletionIntegers :=
  (kw_ffgc_adicCompletionComap F W).restrict _ _
    fun _ hx => kw_ffgc_adicCompletionComap_mem_integers F W hx

@[simp]
theorem kw_ffgc_adicCompletionComapIntegers_coe
    (x : (W.restrict F).adicCompletionIntegers) :
    (kw_ffgc_adicCompletionComapIntegers F W x : W.adicCompletion)
      = kw_ffgc_adicCompletionComap F W (x : (W.restrict F).adicCompletion) := rfl

end IntegerComap

end AlgebraicCurve.Place

set_option autoImplicit false
set_option synthInstance.maxHeartbeats 800000
set_option maxHeartbeats 1600000

noncomputable section

open Polynomial IsLocalRing IsDedekindDomain

namespace AlgebraicCurve.Place

section CompletionAlgebra

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

scoped instance kw_ffgc_algebraAdicCompletionComap :
    Algebra (W.restrict F).adicCompletion W.adicCompletion :=
  (kw_ffgc_adicCompletionComap F W).toAlgebra

theorem kw_ffgc_algebraMap_adicCompletionComap_eq :
    algebraMap (W.restrict F).adicCompletion W.adicCompletion
      = kw_ffgc_adicCompletionComap F W := rfl

scoped instance kw_ffgc_algebraAdicCompletionComapIntegers :
    Algebra (W.restrict F).adicCompletionIntegers W.adicCompletionIntegers :=
  (kw_ffgc_adicCompletionComapIntegers F W).toAlgebra

scoped instance kw_ffgc_algebraAdicCompletionIntegersToCompletion :
    Algebra (W.restrict F).adicCompletionIntegers W.adicCompletion :=
  ((kw_ffgc_adicCompletionComap F W).comp
    (algebraMap (W.restrict F).adicCompletionIntegers (W.restrict F).adicCompletion)).toAlgebra

instance kw_ffgc_isScalarTower_integersCompletionCompletion :
    IsScalarTower (W.restrict F).adicCompletionIntegers
      (W.restrict F).adicCompletion W.adicCompletion :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

instance kw_ffgc_isScalarTower_integersIntegersCompletion :
    IsScalarTower (W.restrict F).adicCompletionIntegers
      W.adicCompletionIntegers W.adicCompletion :=
  IsScalarTower.of_algebraMap_eq fun x => (kw_ffgc_adicCompletionComapIntegers_coe F W x).symm

end CompletionAlgebra

section SpectralSetup

open scoped Valued NNReal WithZero

open WithZeroMulInt Valuation.IsRankOneDiscrete

variable {K F : Type*} [Field K] [Field F] [Algebra K F] (V : Place K F)

@[implicit_reducible]
noncomputable def kw_ffgc_rankOne_adicCompletion :
    (Valued.v : Valuation V.adicCompletion ℤᵐ⁰).RankOne :=
  Valuation.IsRankOneDiscrete.rankOne _ (one_lt_two (α := ℝ≥0))

end SpectralSetup

section AbsoluteValue

open scoped Valued NNReal WithZero

open WithZeroMulInt Valuation.IsRankOneDiscrete

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

noncomputable def kw_ffgc_absoluteValue : AbsoluteValue W.adicCompletion ℝ :=
  letI := kw_ffgc_rankOne_adicCompletion W
  have hr : (0 : ℝ) < ((W.ramificationIndex F : ℝ))⁻¹ :=
    inv_pos.mpr (Nat.cast_pos.mpr (W.ramificationIndex_pos (F := F)))
  { toFun := fun y => ‖y‖ ^ ((W.ramificationIndex F : ℝ))⁻¹
    map_mul' := fun x y => by rw [norm_mul, Real.mul_rpow (norm_nonneg x) (norm_nonneg y)]
    nonneg' := fun x => Real.rpow_nonneg (norm_nonneg x) _
    eq_zero' := fun x => by
      rw [Real.rpow_eq_zero_iff_of_nonneg (norm_nonneg x), norm_eq_zero]
      exact ⟨fun h => h.1, fun h => ⟨h, hr.ne'⟩⟩
    add_le' := fun x y => by
      have hmax : ‖x + y‖ ≤ max ‖x‖ ‖y‖ := Valuation.norm_add_le Valued.v x y
      refine (Real.rpow_le_rpow (norm_nonneg _) hmax hr.le).trans ?_
      rcases max_cases ‖x‖ ‖y‖ with ⟨hm, _⟩ | ⟨hm, _⟩ <;> rw [hm]
      · exact le_add_of_nonneg_right (Real.rpow_nonneg (norm_nonneg _) _)
      · exact le_add_of_nonneg_left (Real.rpow_nonneg (norm_nonneg _) _) }

end AbsoluteValue

section ClosedAdjoin

open scoped Valued NNReal WithZero

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

instance kw_ffgc_continuousSMul_adicCompletionComap :
    ContinuousSMul (W.restrict F).adicCompletion W.adicCompletion :=
  continuousSMul_of_algebraMap _ _ (by
    rw [kw_ffgc_algebraMap_adicCompletionComap_eq]
    exact kw_ffgc_continuous_adicCompletionComap F W)

end ClosedAdjoin

end AlgebraicCurve.Place

set_option autoImplicit false
set_option synthInstance.maxHeartbeats 800000
set_option maxHeartbeats 1600000

noncomputable section

open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero

open scoped Valued WithZero

namespace AlgebraicCurve.Place

section FiniteDimensional

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

theorem kw_ffgc_adicCompletionComap_algebraMap_algebraMap (c : F) :
    algebraMap F' W.adicCompletion (algebraMap F F' c)
      = algebraMap (W.restrict F).adicCompletion W.adicCompletion
          (algebraMap F (W.restrict F).adicCompletion c) := by
  rw [kw_ffgc_algebraMap_adicCompletionComap_eq,
    show algebraMap F (W.restrict F).adicCompletion c
      = ((WithVal.toVal ((W.restrict F).heightOneSpectrum.valuation F) c
          : WithVal ((W.restrict F).heightOneSpectrum.valuation F))
          : (W.restrict F).adicCompletion) from rfl,
    kw_ffgc_adicCompletionComap_coe]
  rfl

theorem kw_ffgc_algebraMap_smul_algebraMap (c : F) (b : F') :
    algebraMap F (W.restrict F).adicCompletion c • algebraMap F' W.adicCompletion b
      = algebraMap F' W.adicCompletion (c • b) := by
  rw [Algebra.smul_def, Algebra.smul_def, map_mul,
    kw_ffgc_adicCompletionComap_algebraMap_algebraMap]

def kw_ffgc_completionLinearCombination {ι : Type*} [Fintype ι] (b : Module.Basis ι F F') :
    (ι → (W.restrict F).adicCompletion)
      →ₗ[(W.restrict F).adicCompletion] W.adicCompletion :=
  Fintype.linearCombination (W.restrict F).adicCompletion
    (fun i => algebraMap F' W.adicCompletion (b i))

theorem kw_ffgc_denseRange_completionLinearCombination {ι : Type*} [Fintype ι]
    (b : Module.Basis ι F F') :
    DenseRange (kw_ffgc_completionLinearCombination F W b) := by
  apply (IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap F' W.heightOneSpectrum).mono
  rintro _ ⟨l, rfl⟩
  refine ⟨fun i => algebraMap F (W.restrict F).adicCompletion (b.repr l i), ?_⟩
  simp only [kw_ffgc_completionLinearCombination, Fintype.linearCombination_apply,
    kw_ffgc_algebraMap_smul_algebraMap, ← map_sum]
  congr 1
  exact b.sum_repr l

instance kw_ffgc_finiteDimensional_adicCompletion [FiniteDimensional F F'] :
    FiniteDimensional (W.restrict F).adicCompletion W.adicCompletion := by
  letI := kw_ffgc_rankOne_adicCompletion (W.restrict F)
  letI : NontriviallyNormedField (W.restrict F).adicCompletion :=
    Valued.toNontriviallyNormedField (W.restrict F).adicCompletion ℤᵐ⁰
  let b := Module.finBasis F F'
  exact Module.Finite.of_surjective (kw_ffgc_completionLinearCombination F W b) (by
    rw [← Set.range_eq_univ, ← LinearMap.coe_range,
      ← (LinearMap.range
          (kw_ffgc_completionLinearCombination F W b)).closed_of_finiteDimensional.closure_eq]
    exact (kw_ffgc_denseRange_completionLinearCombination F W b).closure_range)

end FiniteDimensional

section CompletionTrace

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

abbrev kw_ffgc_completionTrace [FiniteDimensional F F'] :
    W.adicCompletion →ₗ[(W.restrict F).adicCompletion] (W.restrict F).adicCompletion :=
  Algebra.trace (W.restrict F).adicCompletion W.adicCompletion

def kw_ffgc_completionTraceF' [FiniteDimensional F F'] : F' →ₗ[F] (W.restrict F).adicCompletion :=
  { toFun := fun g => kw_ffgc_completionTrace F W (algebraMap F' W.adicCompletion g)
    map_add' := fun x y => by simp only [map_add]
    map_smul' := fun c x => by
      simp only [Algebra.smul_def, map_mul, RingHom.id_apply,
        kw_ffgc_adicCompletionComap_algebraMap_algebraMap]
      rw [← Algebra.smul_def, LinearMap.map_smul, Algebra.smul_def]
      rfl }

end CompletionTrace

end AlgebraicCurve.Place

set_option autoImplicit false
set_option maxHeartbeats 1600000
set_option synthInstance.maxHeartbeats 800000
set_option linter.unusedSectionVars false

open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain

noncomputable section

namespace AlgebraicCurve

section LocalResidueCompletion

variable {K E : Type*} [Field K] [Field E] [Algebra K E]

theorem kwHgfV352_valued_algebraMap_adicCompletion (v : Place K E) (x : E) :
    Valued.v (algebraMap E v.adicCompletion x) = v.heightOneSpectrum.valuation E x := by
  have h := IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation'
    (K := E) v.heightOneSpectrum x
  first
    | exact h
    | (rw [IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion]; exact h)

namespace Place

private theorem mem_of_ord_nonneg_placeCompletionAux {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring := by
  obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible v.toValuationSubring
  obtain ⟨u, hu⟩ := v.exists_unit_mul_zpow hf hπ
  rw [hu, show v.ord f = (((v.ord f).toNat : ℕ) : ℤ) from (Int.toNat_of_nonneg h).symm,
    zpow_natCast]
  exact mul_mem (u : v.toValuationSubring).2 (pow_mem (π : v.toValuationSubring).2 _)

private theorem ord_nonneg_of_mem_placeCompletionAux {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f := by
  rcases eq_or_ne f 0 with rfl | hf0
  · simp
  obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible v.toValuationSubring
  obtain ⟨n, u, hu⟩ :=
    IsDiscreteValuationRing.eq_unit_mul_pow_irreducible
      (x := (⟨f, hf⟩ : v.toValuationSubring)) (by simpa [Subtype.ext_iff] using hf0) hπ
  have hcoe : f = ((u : v.toValuationSubring) : F) * ((π : F) ^ (n : ℤ)) := by
    have h := congrArg (Subtype.val) hu
    push_cast at h
    rw [zpow_natCast]
    exact h
  rw [hcoe, v.ord_unit_smul_zpow u hπ (n : ℤ)]
  exact Int.natCast_nonneg n

end Place

theorem kwHgfV352_algebraMap_mem_adicCompletionIntegers_iff (v : Place K E) (x : E) :
    algebraMap E v.adicCompletion x ∈ v.adicCompletionIntegers ↔ x ∈ v.toValuationSubring := by
  rcases eq_or_ne x 0 with rfl | hx0
  · simp only [map_zero]; exact iff_of_true (zero_mem _) (zero_mem _)
  have hval : Valued.v (algebraMap E v.adicCompletion x) = v.adicValuation x :=
    kwHgfV352_valued_algebraMap_adicCompletion v x
  have hne : v.adicValuation x ≠ 0 := v.adicValuation_ne_zero hx0
  have hlog_iff : WithZero.log (v.adicValuation x) ≤ 0 ↔ v.adicValuation x ≤ 1 := by
    rw [WithZero.log_le_iff_le_exp hne, WithZero.exp_zero]
  constructor
  · intro h
    refine v.mem_of_ord_nonneg_placeCompletionAux hx0 (neg_nonneg.mpr ?_)
    exact hlog_iff.mpr (hval ▸ h)
  · intro h
    show Valued.v (algebraMap E v.adicCompletion x) ≤ 1
    rw [hval]
    exact hlog_iff.mp (neg_nonneg.mp (v.ord_nonneg_of_mem_placeCompletionAux h))

theorem kwHgfV352_exists_sub_mem_adicCompletionIntegers (v : Place K E)
    (xh : v.adicCompletion) :
    ∃ x : E, algebraMap E v.adicCompletion x - xh ∈ v.adicCompletionIntegers := by
  have hdense : DenseRange (algebraMap E v.adicCompletion) :=
    IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap E v.heightOneSpectrum
  have hopen : IsOpen ((xh + ·) '' (v.adicCompletionIntegers : Set v.adicCompletion)) :=
    (Homeomorph.addLeft xh).isOpenMap _ (Valued.isOpen_valuationSubring v.adicCompletion)
  have hmem : xh ∈ (xh + ·) '' (v.adicCompletionIntegers : Set v.adicCompletion) :=
    ⟨0, zero_mem _, by simp⟩
  obtain ⟨e, he⟩ := hdense.exists_mem_open hopen ⟨xh, hmem⟩
  obtain ⟨o, hoMem, hoEq⟩ := he
  exact ⟨e, by rw [← hoEq]; simpa using hoMem⟩

end LocalResidueCompletion

end AlgebraicCurve

set_option autoImplicit false
set_option maxHeartbeats 1600000
set_option synthInstance.maxHeartbeats 800000
set_option linter.unusedSectionVars false

open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing

noncomputable section

namespace ModularCurve.KwF4gRRTate

section PoleWindowShift

variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)

theorem algebraMap_K_mem_adicCompletionIntegers (c : K) :
    algebraMap K u.adicCompletion c ∈ u.adicCompletionIntegers := by
  rw [IsScalarTower.algebraMap_apply K L u.adicCompletion]
  exact (kwHgfV352_algebraMap_mem_adicCompletionIntegers_iff u _).mpr (u.algebraMap_mem' c)

def algebraMapKIntegers : K →+* u.adicCompletionIntegers where
  toFun c := ⟨algebraMap K u.adicCompletion c, algebraMap_K_mem_adicCompletionIntegers u c⟩
  map_one' := Subtype.ext (map_one _)
  map_mul' x y := Subtype.ext (map_mul _ x y)
  map_zero' := Subtype.ext (map_zero _)
  map_add' x y := Subtype.ext (map_add _ x y)

instance instAlgebraKAdicCompletionIntegers : Algebra K u.adicCompletionIntegers :=
  (algebraMapKIntegers u).toAlgebra

end PoleWindowShift

end ModularCurve.KwF4gRRTate

end