-- Module: Mathlib.Algebra.Order.Module.HahnEmbedding
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : IsOrderedRing K
inst_3 : Archimedean K
M : Type u_2
inst_4 : AddCommGroup M
inst_5 : LinearOrder M
inst_6 : IsOrderedAddMonoid M
inst_7 : Module K M
inst_8 : IsOrderedModule K M
R : Type u_3
inst_9 : AddCommGroup R
inst_10 : LinearOrder R
inst_11 : Module K R
seed : Seed K M R
f : Partial seed
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
c : FiniteArchimedeanClass M
hx : (↑x : M) ∈ seed.stratum c
hx' : (↑x : M) ∈ seed.baseEmbedding.domain
heq : (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseEmbedding.domain) (↑x : M) hx') : M) = (↑x : M)
fx : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c) :=
  DFinsupp.single (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) c
    (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.stratum c) (↑x : M) hx)
hfx :
  (↑x : M) =
    fx.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
d : FiniteArchimedeanClass M
coeff :
  ∀ (hx : (↑x : M) ∈ seed.stratum d),
    let fx : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c) :=
      DFinsupp.single (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) d
        (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.stratum d) (↑x : M) hx);
    ∀
      (hfx :
        (↑x : M) =
          fx.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
            (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)),
      Eq.{u_3 + 1} (α := R)
        ((seed.coeff d : (a : ↥(seed.stratum d)) → R)
            ((DFinsupp.single (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) d
                  (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.stratum d) (↑x : M) hx) :
                (a : FiniteArchimedeanClass M) → ↥(seed.stratum a))
              d) :
          R)
        (HahnSeries.coeff
            ((single d : (a : R) → R⟦FiniteArchimedeanClass M⟧)
              ((seed.coeff d : (a : ↥(seed.stratum d)) → R)
                (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.stratum d) (↑x : M) hx)))
            d :
          R)
coeff₁ :
  ∀ (hdc : d ≠ c),
    Eq.{u_3 + 1} (α := R)
      ((seed.coeff d : (a : ↥(seed.stratum d)) → R)
          ((DFinsupp.single (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) c
                (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.stratum c) (↑x : M) hx) :
              (a : FiniteArchimedeanClass M) → ↥(seed.stratum a))
            d) :
        R)
      (HahnSeries.coeff
          ((single c : (a : R) → R⟦FiniteArchimedeanClass M⟧)
            ((seed.coeff c : (a : ↥(seed.stratum c)) → R)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.stratum c) (↑x : M) hx)))
          d :
        R)
⊢ Eq.{u_3 + 1} (α := R)
    ((seed.coeff d : (a : ↥(seed.stratum d)) → R)
        ((DFinsupp.single (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) c
              (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.stratum c) (↑x : M) hx) :
            (a : FiniteArchimedeanClass M) → ↥(seed.stratum a))
          d) :
      R)
    (HahnSeries.coeff
        ((single c : (a : R) → R⟦FiniteArchimedeanClass M⟧)
          ((seed.coeff c : (a : ↥(seed.stratum c)) → R)
            (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.stratum c) (↑x : M) hx)))
        d :
      R)

Tactic:
obtain rfl | hdc := eq_or_ne d c

Premises used: eq_or_ne, rfl