ValuationSubring_exists_pow_eq_unit_mul_zpow_of_isAlgebraic_of_isNoetherianRing.lean

theorem eq_one_of_le_one_of_mul_eq_one {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] {a b : Γ}
    (ha : a ≤ 1) (hb : b ≤ 1) (hab : a * b = 1) : a = 1

theorem _root_.ValuationSubring.exists_pow_eq_unit_mul_zpow_of_isAlgebraic_of_isNoetherianRing
    {L : Type u} [Field L] (A : ValuationSubring L)
    (A₀ : Type u) [CommRing A₀] [IsNoetherianRing A₀]
    (ι : A₀ →+* A) (_hι : Function.Injective ι)
    (K₀ : Subfield L)
    (hrange : Set.range (fun a : A₀ => ((ι a : A) : L)) = (A : Set L) ∩ (K₀ : Set L))
    [Algebra.IsAlgebraic K₀ L]
    (π : A) (hπ : π ∈ IsLocalRing.maximalIdeal A) (hπ0 : π ≠ 0) :
    ∀ x : L, x ≠ 0 → ∃ (N : ℕ) (a : ℤ) (u : Aˣ), 0 < N ∧ x ^ N = ((u : A) : L) * (π : L) ^ a := by
  classical
  intro x hx
  let B : ValuationSubring ↥K₀ := A.comap (algebraMap ↥K₀ L)
  have hmemB : ∀ c : ↥K₀, c ∈ B ↔ (c : L) ∈ A := fun c => ValuationSubring.mem_comap
  have hK₀mem : ∀ a : A₀, ((ι a : A) : L) ∈ (K₀ : Set L) := by
    intro a
    have hmem : ((ι a : A) : L) ∈ Set.range (fun a : A₀ => ((ι a : A) : L)) := ⟨a, rfl⟩
    rw [hrange] at hmem
    exact hmem.2
  let f : A₀ →+* ↥B :=
    { toFun := fun a => ⟨⟨((ι a : A) : L), hK₀mem a⟩, (hmemB _).mpr (ι a).2⟩
      map_one' := by
        apply Subtype.ext; apply Subtype.ext
        change ((ι 1 : A) : L) = ((1 : ↥K₀) : L)
        rw [map_one]; rfl
      map_mul' := by
        intro a b
        apply Subtype.ext; apply Subtype.ext
        change ((ι (a * b) : A) : L) = (((ι a : A) : L)) * ((ι b : A) : L)
        rw [map_mul]; rfl
      map_zero' := by
        apply Subtype.ext; apply Subtype.ext
        change ((ι 0 : A) : L) = ((0 : ↥K₀) : L)
        rw [map_zero]; rfl
      map_add' := by
        intro a b
        apply Subtype.ext; apply Subtype.ext
        change ((ι (a + b) : A) : L) = (((ι a : A) : L)) + ((ι b : A) : L)
        rw [map_add]; rfl }
  have hfsurj : Function.Surjective f := by
    intro b
    have hb : ((b : ↥K₀) : L) ∈ (A : Set L) ∩ (K₀ : Set L) := ⟨(hmemB _).mp b.2, (b : ↥K₀).2⟩
    rw [← hrange] at hb
    obtain ⟨a, ha⟩ := hb
    exact ⟨a, Subtype.ext (Subtype.ext ha)⟩
  have : IsNoetherianRing ↥B := isNoetherianRing_of_surjective A₀ (↥B) f hfsurj
  have hπL : ((π : A) : L) ≠ 0 := fun h => hπ0 (Subtype.ext h)
  have hvπ : A.valuation ((π : A) : L) < 1 := (A.valuation_lt_one_iff π).mp hπ
  have hvπ0 : A.valuation ((π : A) : L) ≠ 0 := (Valuation.ne_zero_iff _).mpr hπL
  have hvunit : ∀ w : (↥B)ˣ, A.valuation (((w : ↥B) : ↥K₀) : L) = 1 := by
    intro w
    have h1 : A.valuation (((w : ↥B) : ↥K₀) : L) ≤ 1 :=
      (A.valuation_le_one_iff _).mpr ((hmemB _).mp (w : ↥B).2)
    have h2 : A.valuation ((((w⁻¹ : (↥B)ˣ) : ↥B) : ↥K₀) : L) ≤ 1 :=
      (A.valuation_le_one_iff _).mpr ((hmemB _).mp ((w⁻¹ : (↥B)ˣ) : ↥B).2)
    have h3 : (((w : ↥B) : ↥K₀) : L) * ((((w⁻¹ : (↥B)ˣ) : ↥B) : ↥K₀) : L) = 1 := by
      exact congrArg (fun z : ↥B => ((z : ↥K₀) : L)) w.mul_inv
    exact RatDepthAux.eq_one_of_le_one_of_mul_eq_one h1 h2 (by rw [← map_mul, h3, map_one])
  obtain ⟨n₁, hn₁, c₁, hc₁, hv₁⟩ :=
    ValuationSubring.exists_pow_valuation_eq_valuation_algebraMap_of_isAlgebraic (E := ↥K₀) A hπL
  obtain ⟨n₂, hn₂, c₂, hc₂, hv₂⟩ :=
    ValuationSubring.exists_pow_valuation_eq_valuation_algebraMap_of_isAlgebraic (E := ↥K₀) A hx
  have halg : ∀ c : ↥K₀, algebraMap (↥K₀) L c = (c : L) := fun c => rfl
  rw [halg] at hv₁ hv₂
  have hvc₁ : A.valuation (c₁ : L) < 1 := by
    rw [← hv₁, map_pow]; exact pow_lt_one' hvπ hn₁.ne'
  have hc₁B : c₁ ∈ B := (hmemB _).mpr ((A.valuation_le_one_iff _).mp hvc₁.le)
  have hnf : ¬ IsField ↥B := by
    intro hF
    have hmax : maximalIdeal ↥B = ⊥ := isField_iff_maximalIdeal_eq.mp hF
    have hmem : (⟨c₁, hc₁B⟩ : ↥B) ∈ maximalIdeal ↥B := by
      rw [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff]
      rintro ⟨w, hw⟩
      have h1 := hvunit w
      rw [hw] at h1
      exact absurd h1 hvc₁.ne
    rw [hmax, Ideal.mem_bot] at hmem
    exact hc₁ (congrArg Subtype.val hmem)
  have hDVR : IsDiscreteValuationRing ↥B :=
    ((IsDiscreteValuationRing.TFAE ↥B hnf).out 1 5).mpr (IsBezout.isPrincipal_of_FG _
      (IsNoetherian.noetherian _))
  obtain ⟨ϖ, hϖ⟩ := IsDiscreteValuationRing.exists_irreducible ↥B
  have hϖL : ((ϖ : ↥K₀) : L) ≠ 0 := by
    intro h
    apply hϖ.ne_zero
    apply Subtype.ext; apply Subtype.ext
    exact h
  have hϖ0 : A.valuation ((ϖ : ↥K₀) : L) ≠ 0 := (Valuation.ne_zero_iff _).mpr hϖL
  have key : ∀ y : ↥B, y ≠ 0 → ∃ n : ℕ, A.valuation ((y : ↥K₀) : L) = A.valuation ((ϖ : ↥K₀) : L) ^
    n := by
    intro y hy
    obtain ⟨n, w, hw⟩ := IsDiscreteValuationRing.associated_pow_irreducible hy hϖ
    refine ⟨n, ?_⟩
    have h1 := congrArg (fun z : ↥B => A.valuation ((z : ↥K₀) : L)) hw
    simp only [SubmonoidClass.coe_pow, map_pow] at h1
    have h2 : (((y * (w : ↥B) : ↥B) : ↥K₀) : L) = ((y : ↥K₀) : L) * (((w : ↥B) : ↥K₀) : L) := rfl
    rw [h2, map_mul, hvunit w, mul_one] at h1
    exact h1
  have hval : ∀ c : ↥K₀, c ≠ 0 → ∃ k : ℤ, A.valuation (c : L) = A.valuation ((ϖ : ↥K₀) : L) ^ k :=
    by
    intro c hc
    rcases B.mem_or_inv_mem c with h | h
    · obtain ⟨n, hn⟩ := key ⟨c, h⟩ (fun h0 => hc (congrArg Subtype.val h0))
      exact ⟨n, by rw [zpow_natCast]; exact hn⟩
    · obtain ⟨n, hn⟩ := key ⟨c⁻¹, h⟩ (fun h0 => hc (inv_eq_zero.mp (congrArg Subtype.val h0)))
      refine ⟨-(n : ℤ), ?_⟩
      have hcoe : ((c⁻¹ : ↥K₀) : L) = ((c : ↥K₀) : L)⁻¹ := Subfield.coe_inv K₀ c
      rw [zpow_neg, zpow_natCast, ← hn, hcoe, map_inv₀, inv_inv]
  obtain ⟨k₁, hk₁⟩ := hval c₁ hc₁
  obtain ⟨k₂, hk₂⟩ := hval c₂ hc₂
  have hk₁0 : k₁ ≠ 0 := by
    rintro rfl
    rw [zpow_zero] at hk₁
    exact absurd hvc₁ (by rw [hk₁]; exact lt_irrefl 1)
  have hX0 : A.valuation x ≠ 0 := (Valuation.ne_zero_iff _).mpr hx
  have e₂ : A.valuation x ^ (n₂ : ℤ) = A.valuation ((ϖ : ↥K₀) : L) ^ k₂ := by
    rw [zpow_natCast, ← map_pow, hv₂, hk₂]
  have e₁ : A.valuation ((π : A) : L) ^ (n₁ : ℤ) = A.valuation ((ϖ : ↥K₀) : L) ^ k₁ := by
    rw [zpow_natCast, ← map_pow, hv₁, hk₁]
  obtain ⟨N, a, hN, hNa⟩ : ∃ (N : ℕ) (a : ℤ), 0 < N ∧
      A.valuation x ^ (N : ℤ) = A.valuation ((π : A) : L) ^ a := by
    rcases lt_or_gt_of_ne hk₁0 with hneg | hpos
    · refine ⟨n₂ * (-k₁).toNat, -((n₁ : ℤ) * k₂), Nat.mul_pos hn₂ (by omega), ?_⟩
      have hk : (((-k₁).toNat : ℕ) : ℤ) = -k₁ := Int.toNat_of_nonneg (by omega)
      rw [Nat.cast_mul, hk, zpow_mul, e₂, ← zpow_mul, show k₂ * -k₁ = k₁ * -k₂
        by ring, zpow_mul, ← e₁,
        ← zpow_mul]
      congr 1; ring
    · refine ⟨n₂ * k₁.toNat, (n₁ : ℤ) * k₂, Nat.mul_pos hn₂ (by omega), ?_⟩
      have hk : ((k₁.toNat : ℕ) : ℤ) = k₁ := Int.toNat_of_nonneg hpos.le
      rw [Nat.cast_mul, hk, zpow_mul, e₂, ← zpow_mul, show k₂ * k₁ = k₁ * k₂
        by ring, zpow_mul, ← e₁,
        ← zpow_mul]
  have hπa : ((π : A) : L) ^ a ≠ 0 := zpow_ne_zero a hπL
  have hval1 : A.valuation (x ^ N * (((π : A) : L) ^ a)⁻¹) = 1 := by
    rw [map_mul, map_inv₀, map_zpow₀, map_pow, ← zpow_natCast, hNa, mul_inv_cancel₀ (zpow_ne_zero a
      hvπ0)]
  have hmemA : x ^ N * (((π : A) : L) ^ a)⁻¹ ∈ A := (A.valuation_le_one_iff _).mp hval1.le
  obtain ⟨u, hu⟩ := (A.valuation_eq_one_iff ⟨_, hmemA⟩).mpr hval1
  refine ⟨N, a, u, hN, ?_⟩
  have hcoe : ((u : A) : L) = x ^ N * (((π : A) : L) ^ a)⁻¹ := by rw [hu]
  rw [hcoe, inv_mul_cancel_right₀ hπa]