Basic.lean

/-
Copyright (c) 2021 Aaron Anderson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Aaron Anderson
-/
module

public import Mathlib.Algebra.Notation.Support
public import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
public import Mathlib.Data.Finsupp.Defs
public import Mathlib.Order.WellFoundedSet

/-!
# Hahn Series

If `Γ` is ordered and `R` has zero, then the type `HahnSeries Γ R`, which we denote as `R⟦Γ⟧`,
consists of formal series over `Γ` with coefficients in `R`, whose supports are partially
well-ordered. With further structure on `R` and `Γ`, we can add further structure on `R⟦Γ⟧`, with
the most studied case being when `Γ` is a linearly ordered abelian group and `R` is a field, in
which case `R⟦Γ⟧` is a valued field, with value group `Γ`.

These generalize Laurent series (with value group `ℤ`), and Laurent series are implemented that way
in the file `Mathlib/RingTheory/LaurentSeries.lean`.

## Main Definitions

* If `Γ` is ordered and `R` has zero, then `R⟦Γ⟧` consists of
  formal series over `Γ` with coefficients in `R`, whose supports are partially well-ordered.
* `support x` is the subset of `Γ` whose coefficients are nonzero.
* `single a r` is the Hahn series which has coefficient `r` at `a` and zero otherwise.
* `orderTop x` is a minimal element of `WithTop Γ` where `x` has a nonzero
  coefficient if `x ≠ 0`, and is `⊤` when `x = 0`.
* `order x` is a minimal element of `Γ` where `x` has a nonzero coefficient if `x ≠ 0`, and is zero
  when `x = 0`.
* `map` takes each coefficient of a Hahn series to its target under a zero-preserving map.
* `embDomain` preserves coefficients, but embeds the index set `Γ` in a larger poset.

## References

- [J. van der Hoeven, *Operators on Generalized Power Series*][van_der_hoeven]
-/

@[expose] public section


open Finset Function

noncomputable section

/-- If `Γ` is linearly ordered and `R` has zero, then `R⟦Γ⟧` consists of
  formal series over `Γ` with coefficients in `R`, whose supports are well-founded. -/
@[ext]
structure HahnSeries (Γ : Type*) (R : Type*) [PartialOrder Γ] [Zero R] where
  /-- The coefficient function of a Hahn Series. -/
  coeff : Γ → R
  isPWO_support' : (Function.support coeff).IsPWO

variable {Γ Γ' R S : Type*}

namespace HahnSeries

@[inherit_doc HahnSeries]
scoped syntax:max (priority := high) term noWs "⟦" term "⟧" : term

macro_rules | `($R⟦$M⟧) => `(HahnSeries $M $R)

/-- Unexpander for `HahnSeries`. -/
@[scoped app_unexpander HahnSeries]
meta def unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $M $R) => `($R⟦$M⟧)
  | _ => throw ()

section Zero

variable [PartialOrder Γ] [Zero R]

theorem coeff_injective : Injective (coeff : R⟦Γ⟧ → Γ → R) :=
  fun _ _ => HahnSeries.ext

@[simp]
theorem coeff_inj {x y : R⟦Γ⟧} : x.coeff = y.coeff ↔ x = y :=
  coeff_injective.eq_iff

/-- The support of a Hahn series is just the set of indices whose coefficients are nonzero.
  Notably, it is well-founded. -/
nonrec def support (x : R⟦Γ⟧) : Set Γ :=
  support x.coeff

@[simp]
theorem support_mk (f : Γ → R) (h) : support ⟨f, h⟩ = Function.support f :=
  rfl

@[simp]
theorem isPWO_support (x : R⟦Γ⟧) : x.support.IsPWO :=
  x.isPWO_support'

@[simp]
theorem isWF_support (x : R⟦Γ⟧) : x.support.IsWF :=
  x.isPWO_support.isWF

@[simp]
theorem mem_support (x : R⟦Γ⟧) (a : Γ) : a ∈ x.support ↔ x.coeff a ≠ 0 :=
  .rfl

instance : Zero R⟦Γ⟧ :=
  ⟨{  coeff := 0
      isPWO_support' := by simp }⟩

instance : Inhabited R⟦Γ⟧ :=
  ⟨0⟩

instance [Subsingleton R] : Subsingleton R⟦Γ⟧ :=
  ⟨fun _ _ => HahnSeries.ext (by subsingleton)⟩

theorem coeff_zero' : (0 : R⟦Γ⟧).coeff = 0 :=
  rfl

@[simp]
theorem coeff_zero {a : Γ} : (0 : R⟦Γ⟧).coeff a = 0 :=
  rfl

@[simp]
theorem coeff_fun_eq_zero_iff {x : R⟦Γ⟧} : x.coeff = 0 ↔ x = 0 :=
  coeff_injective.eq_iff' rfl

theorem ne_zero_of_coeff_ne_zero {x : R⟦Γ⟧} {g : Γ} (h : x.coeff g ≠ 0) : x ≠ 0 :=
  mt (fun x0 => (x0.symm ▸ coeff_zero : x.coeff g = 0)) h

@[simp]
theorem support_zero : support (0 : R⟦Γ⟧) = ∅ :=
  Function.support_zero

@[simp]
nonrec theorem support_nonempty_iff {x : R⟦Γ⟧} : x.support.Nonempty ↔ x ≠ 0 := by
  rw [support, support_nonempty_iff, Ne, coeff_fun_eq_zero_iff]

@[simp]
theorem support_eq_empty_iff {x : R⟦Γ⟧} : x.support = ∅ ↔ x = 0 :=
  Function.support_eq_empty_iff.trans coeff_fun_eq_zero_iff

/-- The map of Hahn series induced by applying a zero-preserving map to each coefficient. -/
@[simps]
def map [Zero S] (x : R⟦Γ⟧) {F : Type*} [FunLike F R S] [ZeroHomClass F R S] (f : F) : S⟦Γ⟧ where
  coeff g := f (x.coeff g)
  isPWO_support' := x.isPWO_support.mono <| Function.support_comp_subset (ZeroHomClass.map_zero f) _

@[simp]
protected lemma map_zero [Zero S] (f : ZeroHom R S) : (0 : R⟦Γ⟧).map f = 0 := by
  ext; simp

theorem support_map_subset [Zero S] (x : R⟦Γ⟧) (f : ZeroHom R S) :
    (x.map f).support ⊆ x.support :=
  Function.support_comp_subset (ZeroHomClass.map_zero f) _

/-- Change a `HahnSeries` with coefficients in a `HahnSeries` to a `HahnSeries` on a Lex product. -/
def ofIterate [PartialOrder Γ'] (x : R⟦Γ'⟧⟦Γ⟧) : R⟦Γ ×ₗ Γ'⟧ where
  coeff := fun g => coeff (coeff x g.1) g.2
  isPWO_support' := by
    refine Set.PartiallyWellOrderedOn.subsetProdLex ?_ ?_
    · refine Set.IsPWO.mono x.isPWO_support' ?_
      simp_rw [Set.image_subset_iff, support_subset_iff, Set.mem_preimage, Function.mem_support]
      exact fun _ ↦ ne_zero_of_coeff_ne_zero
    · exact fun a => by simpa [Function.mem_support, ne_eq] using (x.coeff a).isPWO_support'

@[simp]
lemma mk_eq_zero (f : Γ → R) (h) : HahnSeries.mk f h = 0 ↔ f = 0 := by
  simp_rw [HahnSeries.ext_iff, funext_iff, coeff_zero, Pi.zero_apply]

/-- Change a `HahnSeries` on a Lex product to a `HahnSeries` with coefficients in a `HahnSeries`. -/
def toIterate [PartialOrder Γ'] (x : R⟦Γ ×ₗ Γ'⟧) : R⟦Γ'⟧⟦Γ⟧ where
  coeff := fun g => {
    coeff := fun g' => coeff x (g, g')
    isPWO_support' := Set.PartiallyWellOrderedOn.fiberProdLex x.isPWO_support' g
  }
  isPWO_support' := by
    have h₁ : (Function.support fun g => HahnSeries.mk (fun g' => x.coeff (g, g'))
        (Set.PartiallyWellOrderedOn.fiberProdLex x.isPWO_support' g)) = Function.support
        fun g => fun g' => x.coeff (g, g') := by
      simp only [Function.support, ne_eq, mk_eq_zero]
    rw [h₁, Function.support_fun_curry x.coeff]
    exact Set.PartiallyWellOrderedOn.imageProdLex x.isPWO_support'

/-- The equivalence between iterated Hahn series and Hahn series on the lex product. -/
@[simps]
def iterateEquiv [PartialOrder Γ'] : R⟦Γ'⟧⟦Γ⟧ ≃ R⟦Γ ×ₗ Γ'⟧ where
  toFun := ofIterate
  invFun := toIterate
  left_inv := congrFun rfl
  right_inv := congrFun rfl

open Classical in
/-- `single a r` is the Hahn series which has coefficient `r` at `a` and zero otherwise. -/
def single (a : Γ) : ZeroHom R R⟦Γ⟧ where
  toFun r :=
    { coeff := Pi.single a r
      isPWO_support' := (Set.isPWO_singleton a).mono Pi.support_single_subset }
  map_zero' := HahnSeries.ext (Pi.single_zero _)

variable {a b : Γ} {r : R}

@[simp]
theorem coeff_single_same (a : Γ) (r : R) : (single a r).coeff a = r := by
  classical exact Pi.single_eq_same (M := fun _ => R) a r

@[simp]
theorem coeff_single_of_ne (h : b ≠ a) : (single a r).coeff b = 0 := by
  classical exact Pi.single_eq_of_ne (M := fun _ => R) h r

open Classical in
theorem coeff_single : (single a r).coeff b = if b = a then r else 0 := by
  split_ifs with h <;> simp [h]

@[simp]
theorem support_single_of_ne (h : r ≠ 0) : support (single a r) = {a} := by
  classical exact Pi.support_single_of_ne h

theorem support_single_subset : support (single a r) ⊆ {a} := by
  classical exact Pi.support_single_subset

theorem eq_of_mem_support_single {b : Γ} (h : b ∈ support (single a r)) : b = a :=
  support_single_subset h

theorem single_eq_zero : single a (0 : R) = 0 :=
  (single a).map_zero

theorem single_injective (a : Γ) : Function.Injective (single a : R → R⟦Γ⟧) :=
  fun r s rs => by rw [← coeff_single_same a r, ← coeff_single_same a s, rs]

theorem single_ne_zero (h : r ≠ 0) : single a r ≠ 0 := fun con =>
  h (single_injective a (con.trans single_eq_zero.symm))

@[simp]
theorem single_eq_zero_iff {a : Γ} {r : R} : single a r = 0 ↔ r = 0 :=
  map_eq_zero_iff _ <| single_injective a

@[simp]
protected lemma map_single [Zero S] (f : ZeroHom R S) : (single a r).map f = single a (f r) := by
  ext g
  by_cases h : g = a <;> simp [h]

instance [Nonempty Γ] [Nontrivial R] : Nontrivial R⟦Γ⟧ :=
  ⟨by
    obtain ⟨r, s, rs⟩ := exists_pair_ne R
    inhabit Γ
    refine ⟨single default r, single default s, fun con => rs ?_⟩
    rw [← coeff_single_same (default : Γ) r, con, coeff_single_same]⟩

section Order
variable {x : R⟦Γ⟧}

open Classical in
/-- The orderTop of a Hahn series `x` is a minimal element of `WithTop Γ` where `x` has a nonzero
coefficient if `x ≠ 0`, and is `⊤` when `x = 0`. -/
def orderTop (x : R⟦Γ⟧) : WithTop Γ :=
  if h : x = 0 then ⊤ else x.isWF_support.min (support_nonempty_iff.2 h)

@[simp]
theorem orderTop_zero : orderTop (0 : R⟦Γ⟧) = ⊤ :=
  dif_pos rfl

@[simp]
theorem orderTop_of_subsingleton [Subsingleton R] : x.orderTop = ⊤ :=
  (Subsingleton.eq_zero x) ▸ orderTop_zero

@[deprecated (since := "2025-08-19")] alias orderTop_of_Subsingleton := orderTop_of_subsingleton

theorem orderTop_of_ne_zero (hx : x ≠ 0) :
    orderTop x = x.isWF_support.min (support_nonempty_iff.2 hx) :=
  dif_neg hx

@[deprecated (since := "2025-08-19")] alias orderTop_of_ne := orderTop_of_ne_zero

@[simp] lemma orderTop_eq_top : orderTop x = ⊤ ↔ x = 0 := by simp [orderTop]
@[simp] lemma orderTop_lt_top : orderTop x < ⊤ ↔ x ≠ 0 := by simp [lt_top_iff_ne_top]
lemma orderTop_ne_top : orderTop x ≠ ⊤ ↔ x ≠ 0 := orderTop_eq_top.not

@[deprecated (since := "2025-08-19")] alias orderTop_eq_top_iff := orderTop_eq_top

@[deprecated orderTop_ne_top (since := "2025-08-19")]
lemma ne_zero_iff_orderTop : x ≠ 0 ↔ orderTop x ≠ ⊤ := orderTop_ne_top.symm

theorem orderTop_eq_of_le {x : R⟦Γ⟧} {g : Γ} (hg : g ∈ x.support)
    (hx : ∀ g' ∈ x.support, g ≤ g') : orderTop x = g := by
  rw [orderTop_of_ne_zero <| support_nonempty_iff.mp <| Set.nonempty_of_mem hg,
    x.isWF_support.min_eq_of_le hg hx]

theorem untop_orderTop_of_ne_zero {x : R⟦Γ⟧} (hx : x ≠ 0) :
    WithTop.untop x.orderTop (orderTop_ne_top.2 hx) =
      x.isWF_support.min (support_nonempty_iff.2 hx) :=
  WithTop.coe_inj.mp ((WithTop.coe_untop (orderTop x) (orderTop_ne_top.2 hx)).trans
    (orderTop_of_ne_zero hx))

theorem coeff_orderTop_ne {x : R⟦Γ⟧} {g : Γ} (hg : x.orderTop = g) :
    x.coeff g ≠ 0 := by
  have h : orderTop x ≠ ⊤ := by simp_all only [ne_eq, WithTop.coe_ne_top, not_false_eq_true]
  have hx : x ≠ 0 := orderTop_ne_top.1 h
  rw [orderTop_of_ne_zero hx, WithTop.coe_eq_coe] at hg
  rw [← hg]
  exact x.isWF_support.min_mem (support_nonempty_iff.2 hx)

theorem orderTop_ne_of_coeff_eq_zero {x : R⟦Γ⟧} {i : Γ} (hx : x.coeff i = 0) :
    x.orderTop ≠ i :=
  fun h ↦ coeff_orderTop_ne h hx

theorem orderTop_le_of_coeff_ne_zero {Γ} [LinearOrder Γ] {x : R⟦Γ⟧}
    {g : Γ} (h : x.coeff g ≠ 0) : x.orderTop ≤ g := by
  rw [orderTop_of_ne_zero (ne_zero_of_coeff_ne_zero h), WithTop.coe_le_coe]
  exact Set.IsWF.min_le _ _ ((mem_support _ _).2 h)

@[simp]
theorem orderTop_single (h : r ≠ 0) : (single a r).orderTop = a :=
  (orderTop_of_ne_zero (single_ne_zero h)).trans
    (WithTop.coe_inj.mpr (support_single_subset
      ((single a r).isWF_support.min_mem (support_nonempty_iff.2 (single_ne_zero h)))))

theorem orderTop_single_le : a ≤ (single a r).orderTop := by
  by_cases hr : r = 0
  · simp only [hr, map_zero, orderTop_zero, le_top]
  · rw [orderTop_single hr]

theorem lt_orderTop_single {g g' : Γ} (hgg' : g < g') : g < (single g' r).orderTop :=
  lt_of_lt_of_le (WithTop.coe_lt_coe.mpr hgg') orderTop_single_le

theorem coeff_eq_zero_of_lt_orderTop {x : R⟦Γ⟧} {i : Γ} (hi : i < x.orderTop) :
    x.coeff i = 0 := by
  rcases eq_or_ne x 0 with (rfl | hx)
  · exact coeff_zero
  contrapose! hi
  rw [← mem_support] at hi
  rw [orderTop_of_ne_zero hx, WithTop.coe_lt_coe]
  exact Set.IsWF.not_lt_min _ _ hi

open Classical in
/-- A leading coefficient of a Hahn series is the coefficient of a lowest-order nonzero term, or
zero if the series vanishes. -/
def leadingCoeff (x : R⟦Γ⟧) : R := x.orderTop.recTopCoe 0 x.coeff

@[simp]
theorem leadingCoeff_zero : leadingCoeff (0 : R⟦Γ⟧) = 0 := by simp [leadingCoeff]

theorem leadingCoeff_of_ne_zero {x : R⟦Γ⟧} (hx : x ≠ 0) :
    x.leadingCoeff = x.coeff (x.orderTop.untop <| orderTop_ne_top.2 hx) := by
  simp [leadingCoeff, orderTop, hx]

@[deprecated (since := "2025-08-19")] alias leadingCoeff_of_ne := leadingCoeff_of_ne_zero

@[simp]
theorem leadingCoeff_eq_zero {x : R⟦Γ⟧} : x.leadingCoeff = 0 ↔ x = 0 := by
  obtain rfl | hx := eq_or_ne x 0 <;> simp [leadingCoeff_of_ne_zero, coeff_orderTop_ne, *]

theorem leadingCoeff_ne_zero {x : R⟦Γ⟧} : x.leadingCoeff ≠ 0 ↔ x ≠ 0 :=
  leadingCoeff_eq_zero.not

@[deprecated (since := "2025-08-19")] alias leadingCoeff_eq_iff := leadingCoeff_eq_zero
@[deprecated (since := "2025-08-19")] alias leadingCoeff_ne_iff := leadingCoeff_ne_zero

@[simp]
theorem leadingCoeff_of_single {a : Γ} {r : R} : leadingCoeff (single a r) = r := by
  by_cases h : r = 0 <;> simp [leadingCoeff, h]

theorem coeff_untop_eq_leadingCoeff {x : R⟦Γ⟧} (hx) :
    x.coeff (x.orderTop.untop hx) = x.leadingCoeff := by
  rw [orderTop_ne_top] at hx
  rw [leadingCoeff_of_ne_zero hx, (WithTop.untop_eq_iff _).mpr (orderTop_of_ne_zero hx)]

variable [Zero Γ]

open Classical in
/-- The order of a nonzero Hahn series `x` is a minimal element of `Γ` where `x` has a
  nonzero coefficient, the order of 0 is 0. -/
def order (x : R⟦Γ⟧) : Γ :=
  if h : x = 0 then 0 else x.isWF_support.min (support_nonempty_iff.2 h)

@[simp]
theorem order_zero : order (0 : R⟦Γ⟧) = 0 :=
  dif_pos rfl

theorem order_of_ne {x : R⟦Γ⟧} (hx : x ≠ 0) :
    order x = x.isWF_support.min (support_nonempty_iff.2 hx) :=
  dif_neg hx

theorem order_eq_orderTop_of_ne_zero (hx : x ≠ 0) : order x = orderTop x := by
  rw [order_of_ne hx, orderTop_of_ne_zero hx]

@[deprecated (since := "2025-08-19")] alias order_eq_orderTop_of_ne := order_eq_orderTop_of_ne_zero

@[simp]
theorem coeff_order_eq_zero {x : R⟦Γ⟧} : x.coeff x.order = 0 ↔ x = 0 := by
  refine ⟨not_imp_not.1 fun hx ↦ ?_, by simp +contextual⟩
  rw [order_of_ne hx]
  exact x.isWF_support.min_mem (support_nonempty_iff.2 hx)

@[deprecated coeff_order_eq_zero (since := "2025-12-09")]
theorem coeff_order_ne_zero {x : R⟦Γ⟧} (hx : x ≠ 0) : x.coeff x.order ≠ 0 :=
  coeff_order_eq_zero.not.2 hx

theorem order_le_of_coeff_ne_zero {Γ} [Zero Γ] [LinearOrder Γ] {x : R⟦Γ⟧}
    {g : Γ} (h : x.coeff g ≠ 0) : x.order ≤ g :=
  le_trans (le_of_eq (order_of_ne (ne_zero_of_coeff_ne_zero h)))
    (Set.IsWF.min_le _ _ ((mem_support _ _).2 h))

@[simp]
theorem order_single (h : r ≠ 0) : (single a r).order = a :=
  (order_of_ne (single_ne_zero h)).trans
    (support_single_subset
      ((single a r).isWF_support.min_mem (support_nonempty_iff.2 (single_ne_zero h))))

theorem coeff_eq_zero_of_lt_order {x : R⟦Γ⟧} {i : Γ} (hi : i < x.order) : x.coeff i = 0 := by
  rcases eq_or_ne x 0 with (rfl | hx)
  · simp
  contrapose! hi
  rw [← mem_support] at hi
  rw [order_of_ne hx]
  exact Set.IsWF.not_lt_min _ _ hi

theorem zero_lt_orderTop_iff {x : R⟦Γ⟧} (hx : x ≠ 0) :
    0 < x.orderTop ↔ 0 < x.order := by
  simp_all [orderTop_of_ne_zero hx, order_of_ne hx]

theorem zero_lt_orderTop_of_order {x : R⟦Γ⟧} (hx : 0 < x.order) : 0 < x.orderTop := by
  by_cases h : x = 0
  · simp_all only [order_zero, lt_self_iff_false]
  · exact (zero_lt_orderTop_iff h).mpr hx

theorem zero_le_orderTop_iff {x : R⟦Γ⟧} : 0 ≤ x.orderTop ↔ 0 ≤ x.order := by
  by_cases h : x = 0
  · simp_all
  · simp_all [order_of_ne h, orderTop_of_ne_zero h]

theorem leadingCoeff_eq {x : R⟦Γ⟧} : x.leadingCoeff = x.coeff x.order := by
  by_cases h : x = 0
  · rw [h, leadingCoeff_zero, coeff_zero]
  · simp [leadingCoeff_of_ne_zero, orderTop_of_ne_zero, order_of_ne, h]

end Order

section Finsupp

/-- Create a `HahnSeries` with a `Finsupp` as coefficients. -/
def ofFinsupp : ZeroHom (Γ →₀ R) R⟦Γ⟧ where
  toFun f := { coeff := f, isPWO_support' := f.finite_support.isPWO }
  map_zero' := by simp

@[simp]
theorem coeff_ofFinsupp (f : Γ →₀ R) (a : Γ) : (ofFinsupp f).coeff a = f a := rfl

end Finsupp

section Domain

variable [PartialOrder Γ']

open Classical in
/-- Extends the domain of a `HahnSeries` by an `OrderEmbedding`. -/
def embDomain (f : Γ ↪o Γ') : R⟦Γ⟧ → R⟦Γ'⟧ := fun x =>
  { coeff := fun b : Γ' => if h : b ∈ f '' x.support then x.coeff (Classical.choose h) else 0
    isPWO_support' :=
      (x.isPWO_support.image_of_monotone f.monotone).mono fun b hb => by
        contrapose! hb
        rw [Function.mem_support, dif_neg hb, Classical.not_not] }

@[simp]
theorem embDomain_coeff {f : Γ ↪o Γ'} {x : R⟦Γ⟧} {a : Γ} :
    (embDomain f x).coeff (f a) = x.coeff a := by
  rw [embDomain]
  dsimp only
  by_cases ha : a ∈ x.support
  · rw [dif_pos (Set.mem_image_of_mem f ha)]
    exact congr rfl (f.injective (Classical.choose_spec (Set.mem_image_of_mem f ha)).2)
  · rw [dif_neg, Classical.not_not.1 fun c => ha ((mem_support _ _).2 c)]
    contrapose! ha
    obtain ⟨b, hb1, hb2⟩ := (Set.mem_image _ _ _).1 ha
    rwa [f.injective hb2] at hb1

@[simp]
theorem embDomain_mk_coeff {f : Γ → Γ'} (hfi : Function.Injective f)
    (hf : ∀ g g' : Γ, f g ≤ f g' ↔ g ≤ g') {x : R⟦Γ⟧} {a : Γ} :
    (embDomain ⟨⟨f, hfi⟩, hf _ _⟩ x).coeff (f a) = x.coeff a :=
  embDomain_coeff

theorem embDomain_notin_image_support {f : Γ ↪o Γ'} {x : R⟦Γ⟧} {b : Γ'}
    (hb : b ∉ f '' x.support) : (embDomain f x).coeff b = 0 :=
  dif_neg hb

theorem support_embDomain_subset {f : Γ ↪o Γ'} {x : R⟦Γ⟧} :
    support (embDomain f x) ⊆ f '' x.support := by
  intro g hg
  contrapose! hg
  rw [mem_support, embDomain_notin_image_support hg, Classical.not_not]

theorem embDomain_notin_range {f : Γ ↪o Γ'} {x : R⟦Γ⟧} {b : Γ'} (hb : b ∉ Set.range f) :
    (embDomain f x).coeff b = 0 :=
  embDomain_notin_image_support fun con => hb (Set.image_subset_range _ _ con)

@[simp]
theorem embDomain_zero {f : Γ ↪o Γ'} : embDomain f (0 : R⟦Γ⟧) = 0 := by
  ext
  simp [embDomain_notin_image_support]

@[simp]
theorem embDomain_single {f : Γ ↪o Γ'} {g : Γ} {r : R} :
    embDomain f (single g r) = single (f g) r := by
  ext g'
  by_cases h : g' = f g
  · simp [h]
  rw [embDomain_notin_image_support, coeff_single_of_ne h]
  by_cases hr : r = 0
  · simp [hr]
  rwa [support_single_of_ne hr, Set.image_singleton, Set.mem_singleton_iff]

theorem embDomain_injective {f : Γ ↪o Γ'} :
    Function.Injective (embDomain f : R⟦Γ⟧ → R⟦Γ'⟧) := fun x y xy => by
  ext g
  rw [HahnSeries.ext_iff, funext_iff] at xy
  have xyg := xy (f g)
  rwa [embDomain_coeff, embDomain_coeff] at xyg

@[simp]
theorem orderTop_embDomain {Γ : Type*} [LinearOrder Γ] {f : Γ ↪o Γ'} {x : R⟦Γ⟧} :
    (embDomain f x).orderTop = WithTop.map f x.orderTop := by
  obtain rfl | hx := eq_or_ne x 0
  · simp
  rw [← WithTop.coe_untop x.orderTop (by simpa using hx), WithTop.map_coe]
  apply orderTop_eq_of_le
  · simpa using coeff_orderTop_ne (by simp)
  intro y hy
  obtain ⟨z, hz, rfl⟩ :=
    (Set.mem_image _ _ _).mp <| Set.mem_of_subset_of_mem support_embDomain_subset hy
  rw [OrderEmbedding.le_iff_le, WithTop.untop_le_iff]
  apply orderTop_le_of_coeff_ne_zero
  simpa using hz

end Domain

end Zero

section LocallyFiniteLinearOrder

variable [Zero R] [LinearOrder Γ]

theorem forallLTEqZero_supp_BddBelow (f : Γ → R) (n : Γ) (hn : ∀ (m : Γ), m < n → f m = 0) :
    BddBelow (Function.support f) := by
  simp only [BddBelow, Set.Nonempty, lowerBounds]
  use n
  intro m hm
  rw [Function.mem_support, ne_eq] at hm
  exact not_lt.mp (mt (hn m) hm)

theorem BddBelow_zero [Nonempty Γ] : BddBelow (Function.support (0 : Γ → R)) := by
  simp only [Function.support_zero, bddBelow_empty]

variable [LocallyFiniteOrder Γ]

theorem suppBddBelow_supp_PWO (f : Γ → R) (hf : BddBelow (Function.support f)) :
    (Function.support f).IsPWO :=
  hf.isWF.isPWO

/-- Construct a Hahn series from any function whose support is bounded below. -/
@[simps]
def ofSuppBddBelow (f : Γ → R) (hf : BddBelow (Function.support f)) : R⟦Γ⟧ where
  coeff := f
  isPWO_support' := suppBddBelow_supp_PWO f hf

@[simp]
theorem zero_ofSuppBddBelow [Nonempty Γ] : ofSuppBddBelow 0 BddBelow_zero = (0 : R⟦Γ⟧) :=
  rfl

theorem order_ofForallLtEqZero [Zero Γ] (f : Γ → R) (hf : f ≠ 0) (n : Γ)
    (hn : ∀ (m : Γ), m < n → f m = 0) :
    n ≤ order (ofSuppBddBelow f (forallLTEqZero_supp_BddBelow f n hn)) := by
  dsimp only [order]
  by_cases h : ofSuppBddBelow f (forallLTEqZero_supp_BddBelow f n hn) = 0
  cases h
  · exact (hf rfl).elim
  simp_all only [dite_false]
  rw [Set.IsWF.le_min_iff]
  intro m hm
  rw [HahnSeries.support, Function.mem_support, ne_eq] at hm
  exact not_lt.mp (mt (hn m) hm)

end LocallyFiniteLinearOrder

section Truncate
variable [Zero R]

/-- Zeroes out coefficients of a `HahnSeries` at indices not less than `c`. -/
def truncLT [PartialOrder Γ] [DecidableLT Γ] (c : Γ) : ZeroHom R⟦Γ⟧ R⟦Γ⟧ where
  toFun x :=
    { coeff i := if i < c then x.coeff i else 0
      isPWO_support' := Set.IsPWO.mono x.isPWO_support (by simp) }
  map_zero' := by ext; simp

theorem support_truncLT [PartialOrder Γ] [DecidableLT Γ] (c : Γ) (x : R⟦Γ⟧) :
    (truncLT c x).support = {y ∈ x.support | y < c} := by
  simp [truncLT, Function.support, and_comm]

theorem support_truncLT_subset [PartialOrder Γ] [DecidableLT Γ] (c : Γ) (x : R⟦Γ⟧) :
    (truncLT c x).support ⊆ x.support := by
  rw [support_truncLT]
  exact Set.sep_subset ..

@[simp]
protected theorem coeff_truncLT [PartialOrder Γ] [DecidableLT Γ] (c : Γ) (x : R⟦Γ⟧) (i : Γ) :
    (truncLT c x).coeff i = if i < c then x.coeff i else 0 := rfl

theorem coeff_truncLT_of_lt [PartialOrder Γ] [DecidableLT Γ] {c i : Γ} (h : i < c) (x : R⟦Γ⟧) :
    (truncLT c x).coeff i = x.coeff i := by
  simp [h]

theorem coeff_truncLT_of_le [LinearOrder Γ] {c i : Γ} (h : c ≤ i) (x : R⟦Γ⟧) :
    (truncLT c x).coeff i = 0 := by
  simp [h]

end Truncate

end HahnSeries