awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (↑x : M) ∈ seed.baseEmbedding.domain

Tactic:
have hx' : x.val ∈ seed.baseEmbedding.domain := seed.mem_domain_baseEmbedding hx
-- 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
⊢ (↑(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
-- 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)
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)))
⊢ (↑(↑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)))

Tactic:
rw [← f.prop.baseEmbedding_le.2 heq]

Premises used: HahnEmbedding.IsPartial.baseEmbedding_le, And.right, Subtype.prop
-- 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)
⊢ (↑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:
simp [fx, DFinsupp.sum_single_index]

Premises used: DFinsupp.sum_single_index
-- 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)
⊢ (↑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]
-- 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)
coeff :
  ∀ (d : FiniteArchimedeanClass M),
    Eq.{u_3 + 1} (α := R)
      (HahnSeries.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)
      (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)
⊢ 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)

Tactic:
ext d
-- 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 :
  Eq.{u_3 + 1} (α := R)
    ((seed.coeff d : (a : ↥(seed.stratum d)) → R) ((fx : (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)
    (HahnSeries.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)
    (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)

Tactic:
rw [seed.coeff_baseEmbedding hfx]

Premises used: HahnEmbedding.Seed.coeff_baseEmbedding
-- 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 :
  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) ((fx : (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:
unfold fx
-- 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
hx' : (↑x : M) ∈ seed.baseEmbedding.domain
heq : (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseEmbedding.domain) (↑x : M) hx') : M) = (↑x : M)
d : FiniteArchimedeanClass M
hx : (↑x : M) ∈ seed.stratum d
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:
simp
-- 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
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)
    (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:
simp [HahnSeries.coeff_single_of_ne hdc, hdc.symm]

Premises used: Ne.symm, HahnSeries.coeff_single_of_ne
-- 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
inst_12 : IsOrderedAddMonoid R
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
simp_rw :
  Eq (α := ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk x) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk y) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))) ↔
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))
⊢ Eq (α := ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      (ArchimedeanClass.mk
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          x))
      (ArchimedeanClass.mk
        ((↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
            ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
          y)) ↔
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))

Tactic:
simp_rw [← toOrderAddMonoidHom_apply, ← orderHom_mk]

Premises used: HahnEmbedding.Partial.toOrderAddMonoidHom_apply, ArchimedeanClass.orderHom_mk
-- 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
inst_12 : IsOrderedAddMonoid R
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
trans :
  Eq (α := ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk x) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk y) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))) ↔
    Eq (α := ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) (ArchimedeanClass.mk x)
      (ArchimedeanClass.mk y)
trans₁ :
  Eq (α := ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) (ArchimedeanClass.mk x)
      (ArchimedeanClass.mk y) ↔
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))
⊢ Eq (α := ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk x) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk y) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))) ↔
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))

Tactic:
trans ArchimedeanClass.mk x = .mk y

Premises used: ArchimedeanClass.mk
-- 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
inst_12 : IsOrderedAddMonoid R
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ Eq (α := ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk x) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk y) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))) ↔
    Eq (α := ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) (ArchimedeanClass.mk x)
      (ArchimedeanClass.mk y)

Tactic:
Function.Injective.eq_iff <| orderHom_injective <| toOrderAddMonoidHom_injective _

Premises used: Function.Injective.eq_iff, ArchimedeanClass.orderHom_injective
-- 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
inst_12 : IsOrderedAddMonoid R
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ Eq (α := ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk x) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R)))
      ((orderHom f.toOrderAddMonoidHom :
            (a : ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) →
              ArchimedeanClass (Lex R⟦FiniteArchimedeanClass M⟧))
          (ArchimedeanClass.mk y) :
        ArchimedeanClass (Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))) ↔
    Eq (α := ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) (ArchimedeanClass.mk x)
      (ArchimedeanClass.mk y)

Tactic:
exact Function.Injective.eq_iff <| orderHom_injective <| toOrderAddMonoidHom_injective _

Premises used: Function.Injective.eq_iff, ArchimedeanClass.orderHom_injective, HahnEmbedding.Partial.toOrderAddMonoidHom_injective
-- 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
inst_12 : IsOrderedAddMonoid R
x y : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
simp_rw :
  ((∃ (m : ℕ), |y| ≤ m • |x|) ∧ ∃ (n : ℕ), |x| ≤ n • |y|) ↔
    (∃ (m : ℕ), |(↑y : M)| ≤ m • |(↑x : M)|) ∧ ∃ (n : ℕ), |(↑x : M)| ≤ n • |(↑y : M)|
⊢ Eq (α := ArchimedeanClass ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) (ArchimedeanClass.mk x)
      (ArchimedeanClass.mk y) ↔
    Eq (α := ArchimedeanClass M) (ArchimedeanClass.mk (↑x : M)) (ArchimedeanClass.mk (↑y : M))

Tactic:
simp_rw [mk_eq_mk]

Premises used: ArchimedeanClass.mk_eq_mk