awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : (↑x : M) ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(seed.stratum x)) ↦ (↑xi : M)) =
    (↑x : M)
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) :=
  DFinsupp.mk (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
    (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)))
    fun
      (d :
        (↑(↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) :
              Set (FiniteArchimedeanClass M)) :
          Type u_2)) ↦
    if (↑c : ArchimedeanClass M) ≤ (↑(↑d : FiniteArchimedeanClass M) : ArchimedeanClass M) then 0
    else (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) (↑d : FiniteArchimedeanClass M)
d : FiniteArchimedeanClass M
hdc : d < c
hcd : ¬(↑c : ArchimedeanClass M) ≤ (↑d : ArchimedeanClass M)
⊢ (DFinsupp.mk (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
          (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)))
          fun
            (d :
              (↑(↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) :
                    Set (FiniteArchimedeanClass M)) :
                Type u_2)) ↦
          if (↑c : ArchimedeanClass M) ≤ (↑(↑d : FiniteArchimedeanClass M) : ArchimedeanClass M) then 0
          else (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) (↑d : FiniteArchimedeanClass M) :
        (a : FiniteArchimedeanClass M) → ↥(seed.stratum a))
      d =
    (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) d
have refine_2 : (if h : d ∈ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)) then
    (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) d
  else 0) =
  (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) d
Tactic: simp only [DFinsupp.mk_apply, hcd, ↓reduceIte]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (hypothesis)
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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : (↑x : M) ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(seed.stratum x)) ↦ (↑xi : M)) =
    (↑x : M)
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) :=
  DFinsupp.mk (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
    (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)))
    fun
      (d :
        (↑(↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) :
              Set (FiniteArchimedeanClass M)) :
          Type u_2)) ↦
    if (↑c : ArchimedeanClass M) ≤ (↑(↑d : FiniteArchimedeanClass M) : ArchimedeanClass M) then 0
    else (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) (↑d : FiniteArchimedeanClass M)
d : FiniteArchimedeanClass M
hdc : c ≤ d
⊢ Eq.{u_3 + 1} (α := R)
    ((seed.coeff d : (a : ↥(seed.stratum d)) → R)
        ((DFinsupp.mk (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
              (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)))
              fun
                (d :
                  (↑(↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) :
                        Set (FiniteArchimedeanClass M)) :
                    Type u_2)) ↦
              if (↑c : ArchimedeanClass M) ≤ (↑(↑d : FiniteArchimedeanClass M) : ArchimedeanClass M) then 0
              else (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) (↑d : FiniteArchimedeanClass M) :
            (a : FiniteArchimedeanClass M) → ↥(seed.stratum a))
          d) :
      R)
    (0 : R)
have hcd : (↑c : ArchimedeanClass M) ≤ (↑d : ArchimedeanClass M)
Tactic: have hcd : c.val ≤ d.val := hdc
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : (↑x : M) ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(seed.stratum x)) ↦ (↑xi : M)) =
    (↑x : M)
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) :=
  DFinsupp.mk (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
    (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)))
    fun
      (d :
        (↑(↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) :
              Set (FiniteArchimedeanClass M)) :
          Type u_2)) ↦
    if (↑c : ArchimedeanClass M) ≤ (↑(↑d : FiniteArchimedeanClass M) : ArchimedeanClass M) then 0
    else (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) (↑d : FiniteArchimedeanClass M)
d : FiniteArchimedeanClass M
hdc : c ≤ d
hcd : (↑c : ArchimedeanClass M) ≤ (↑d : ArchimedeanClass M)
⊢ Eq.{u_3 + 1} (α := R)
    ((seed.coeff d : (a : ↥(seed.stratum d)) → R)
        ((DFinsupp.mk (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
              (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)))
              fun
                (d :
                  (↑(↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) :
                        Set (FiniteArchimedeanClass M)) :
                    Type u_2)) ↦
              if (↑c : ArchimedeanClass M) ≤ (↑(↑d : FiniteArchimedeanClass M) : ArchimedeanClass M) then 0
              else (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) (↑d : FiniteArchimedeanClass M) :
            (a : FiniteArchimedeanClass M) → ↥(seed.stratum a))
          d) :
      R)
    (0 : R)
have refine_2 : Eq.{u_3 + 1} (α := R)
  ((seed.coeff d : (a : ↥(seed.stratum d)) → R)
      (if h : d ∈ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)) then 0 else 0) :
    R)
  (0 : R)
Tactic: simp only [DFinsupp.mk_apply, hcd, ↓reduceIte]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : (↑x : M) ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(seed.stratum x)) ↦ (↑xi : M)) =
    (↑x : M)
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) :=
  DFinsupp.mk (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))
    (f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)))
    fun
      (d :
        (↑(↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i))) :
              Set (FiniteArchimedeanClass M)) :
          Type u_2)) ↦
    if (↑c : ArchimedeanClass M) ≤ (↑(↑d : FiniteArchimedeanClass M) : ArchimedeanClass M) then 0
    else (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) (↑d : FiniteArchimedeanClass M)
d : FiniteArchimedeanClass M
hdc : c ≤ d
hcd : (↑c : ArchimedeanClass M) ≤ (↑d : ArchimedeanClass M)
⊢ Eq.{u_3 + 1} (α := R)
    ((seed.coeff d : (a : ↥(seed.stratum d)) → R)
        (if h : d ∈ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)) then 0 else 0) :
      R)
    (0 : R)
have h : Eq.{u_2 + 1} (α := ↥(seed.stratum d))
  (if h : d ∈ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)) then 0 else 0) 0
Tactic: convert! LinearMap.map_zero _
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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 : M
c : FiniteArchimedeanClass M
hx : x ∈ seed.stratum c
⊢ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
have apply : x ∈ (↑seed.baseEmbedding.domain : Set M)
Tactic: apply Set.mem_of_subset_of_mem f.prop.baseEmbedding_le.1
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (hypothesis)
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
⊢ (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      x =
    (toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
      ((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)))
have hx' : (↑x : M) ∈ seed.baseEmbedding.domain
Tactic: have hx' : x.val ∈ seed.baseEmbedding.domain := seed.mem_domain_baseEmbedding hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (hypothesis)
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
⊢ (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      x =
    (toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
      ((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)))
have heq : (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseEmbedding.domain) (↑x : M) hx') : M) = (↑x : M)
Tactic: have heq : (⟨x.val, hx'⟩ : seed.baseEmbedding.domain).val = x.val := rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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)
⊢ (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      x =
    (toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
      ((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)))
have rw : (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧)
    (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseEmbedding.domain) (↑x : M) hx') =
  (toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
    ((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)))
Tactic: rw [← f.prop.baseEmbedding_le.2 heq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (hypothesis)
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)
⊢ (↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseEmbedding.domain) (↑x : M) hx') =
    (toLex : (a : R⟦FiniteArchimedeanClass M⟧) → Lex R⟦FiniteArchimedeanClass M⟧)
      ((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)))
have 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)
Tactic: have hfx : x.val = fx.sum fun c ↦ (seed.stratum c).subtype := by
    simp [fx, DFinsupp.sum_single_index]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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)
⊢ Eq (α := HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
    ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseEmbedding.domain) (↑x : M) hx')) :
      HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
    ((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)) :
      HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)
have coeff : ∀ (d : FiniteArchimedeanClass M),
  Eq.{u_3 + 1} (α := R)
    (coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseEmbedding.domain) (↑x : M) hx')))
      d)
    (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)
Tactic: ext d
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ Eq.{u_3 + 1} (α := R)
    (coeff
      ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
        ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseEmbedding.domain) (↑x : M) hx')))
      d)
    (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)
have coeff : Eq.{u_3 + 1} (α := R)
  ((seed.coeff d : (a : ↥(seed.stratum d)) → R) ((fx : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) d) : R)
  (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: rw [seed.coeff_baseEmbedding hfx]
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.HahnEmbedding (goal)
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
⊢ 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)
    (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)
have 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)
      (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)
Tactic: obtain rfl | hdc := eq_or_ne d c
Cleared hypotheses: c, hx, fx, hfx