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
u : ArchimedeanStrata K M
apply : iSup u.stratum' = ⊤
⊢ IsInternal u.stratum'

Tactic:
apply DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top u.iSupIndep_stratum'

Premises used: DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top, HahnEmbedding.ArchimedeanStrata.iSupIndep_stratum'
-- 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
u : ArchimedeanStrata K M
a : Submodule.map u.baseDomain.subtype (iSup u.stratum') = Submodule.map u.baseDomain.subtype ⊤
⊢ iSup u.stratum' = ⊤

Tactic:
apply Submodule.map_injective_of_injective u.baseDomain.subtype_injective

Premises used: Submodule.subtype_injective, Submodule.map_injective_of_injective, HahnEmbedding.ArchimedeanStrata.baseDomain
-- 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
u : ArchimedeanStrata K M
this : ⨆ (i : FiniteArchimedeanClass M), u.baseDomain ⊓ u.stratum i = u.baseDomain
⊢ Submodule.map u.baseDomain.subtype (iSup u.stratum') = Submodule.map u.baseDomain.subtype ⊤

Tactic:
simpa using this
-- 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
u : ArchimedeanStrata K M
a : ⨆ (i : FiniteArchimedeanClass M), u.baseDomain ⊓ u.stratum i = u.baseDomain
⊢ Submodule.map u.baseDomain.subtype (iSup u.stratum') = Submodule.map u.baseDomain.subtype ⊤

Tactic:
suffices ⨆ i, u.baseDomain ⊓ u.stratum i = u.baseDomain by simpa using this
-- 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
u : ArchimedeanStrata K M
a : ∀ (i : FiniteArchimedeanClass M), u.baseDomain ⊓ u.stratum i = u.stratum i
⊢ ⨆ (i : FiniteArchimedeanClass M), u.baseDomain ⊓ u.stratum i = u.baseDomain

Tactic:
apply iSup_congr

Premises used: iSup_congr
-- 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
⊢ u.baseDomain ⊓ u.stratum c = u.stratum c

Tactic:
simpa using le_iSup _ _

Premises used: le_iSup
-- 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
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h :
  (↑x : M) =
    f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
c : FiniteArchimedeanClass M
this :
  (seed.baseDomain.subtype.submoduleComap (seed.stratum c) :
        (a : ↥(Submodule.comap seed.baseDomain.subtype (seed.stratum c))) → ↥(seed.stratum c))
      ((((decompose seed.stratum' : (a : ↥seed.baseDomain) → ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) x :
            ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) :
          (a : FiniteArchimedeanClass M) → ↥(seed.stratum' a))
        c) =
    (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c
⊢ (((seed.hahnCoeff : (a : ↥seed.baseDomain) → ⨁ (x : FiniteArchimedeanClass M), R) x :
          ⨁ (x : FiniteArchimedeanClass M), R) :
        (a : FiniteArchimedeanClass M) → R)
      c =
    (seed.coeff c : (a : ↥(seed.stratum c)) → R) ((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c)

Tactic:
simp [Seed.hahnCoeff, coeff', decomposeLinearEquiv_apply, this]

Premises used: HahnEmbedding.Seed.coeff', HahnEmbedding.Seed.hahnCoeff, DirectSum.decomposeLinearEquiv_apply
-- 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
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h :
  (↑x : M) =
    f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
c : FiniteArchimedeanClass M
suffices :
  (seed.baseDomain.subtype.submoduleComap (seed.stratum c) :
        (a : ↥(Submodule.comap seed.baseDomain.subtype (seed.stratum c))) → ↥(seed.stratum c))
      ((((decompose seed.stratum' : (a : ↥seed.baseDomain) → ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) x :
            ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) :
          (a : FiniteArchimedeanClass M) → ↥(seed.stratum' a))
        c) =
    (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c
⊢ (((seed.hahnCoeff : (a : ↥seed.baseDomain) → ⨁ (x : FiniteArchimedeanClass M), R) x :
          ⨁ (x : FiniteArchimedeanClass M), R) :
        (a : FiniteArchimedeanClass M) → R)
      c =
    (seed.coeff c : (a : ↥(seed.stratum c)) → R) ((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c)

Tactic:
suffices seed.baseDomain.subtype.submoduleComap
      (seed.stratum c) (DirectSum.decompose seed.stratum' x c) = f c by
    simp [Seed.hahnCoeff, coeff', decomposeLinearEquiv_apply, this]
-- 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
x_1 : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h :
  (↑x_1 : M) =
    f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
c_1 c : FiniteArchimedeanClass M
x : ↥(seed.stratum c)
apply : (↑(seed.stratum c) : Set M) ⊆ (↑seed.baseDomain : Set M)
⊢ (↑x : M) ∈ seed.baseDomain

Tactic:
apply Set.mem_of_mem_of_subset x.prop

Premises used: Subtype.prop, Set.mem_of_mem_of_subset
-- 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
x_1 : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h :
  (↑x_1 : M) =
    f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
c_1 c : FiniteArchimedeanClass M
x : ↥(seed.stratum c)
⊢ (↑(seed.stratum c) : Set M) ⊆ (↑seed.baseDomain : Set M)

Tactic:
simpa using le_iSup _ _

Premises used: le_iSup
-- 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
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h :
  (↑x : M) =
    f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
c : FiniteArchimedeanClass M
⊢ ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), (↑x : M) ∈ seed.baseDomain

Tactic:
have hxm {c : FiniteArchimedeanClass M} (x : seed.stratum c) : x.val ∈ seed.baseDomain := by
    apply Set.mem_of_mem_of_subset x.prop
    simpa using le_iSup _ _
-- 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
x_1 : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h :
  (↑x_1 : M) =
    f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
c_1 : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), (↑x : M) ∈ seed.baseDomain
c : FiniteArchimedeanClass M
x : ↥(seed.stratum c)
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseDomain) (↑x : M) ⋯ ∈ seed.stratum' c

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
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h :
  (↑x : M) =
    f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), (↑x : M) ∈ seed.baseDomain
⊢ ∀ (i : FiniteArchimedeanClass M),
    Eq.{u_2 + 1} (α := ↥(seed.stratum' i))
      ((fun (c : FiniteArchimedeanClass M) (x : ↥(seed.stratum c)) ↦
          (Subtype.mk (p := fun (x : ↥seed.baseDomain) ↦ x ∈ seed.stratum' c)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseDomain) (↑x : M) ⋯) ⋯ :
            ↥(seed.stratum' c)))
        i 0)
      0

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
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h :
  (↑x : M) =
    f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), (↑x : M) ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) :=
  DFinsupp.mapRange (β₁ := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) (β₂ :=
    fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum' c))
    (fun (c : FiniteArchimedeanClass M) (x : ↥(seed.stratum c)) ↦
      Subtype.mk (p := fun (x : ↥seed.baseDomain) ↦ x ∈ seed.stratum' c)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseDomain) (↑x : M) ⋯) ⋯)
    ⋯ f
a :
  (↑((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c) : M) =
    (↑((seed.baseDomain.subtype.submoduleComap (seed.stratum c) :
            (a : ↥(Submodule.comap seed.baseDomain.subtype (seed.stratum c))) → ↥(seed.stratum c))
          ((f' : (a : FiniteArchimedeanClass M) → ↥(seed.stratum' a)) c)) :
      M)
⊢ (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c =
    (seed.baseDomain.subtype.submoduleComap (seed.stratum c) :
        (a : ↥(Submodule.comap seed.baseDomain.subtype (seed.stratum c))) → ↥(seed.stratum c))
      ((f' : (a : FiniteArchimedeanClass M) → ↥(seed.stratum' a)) c)

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- 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
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h :
  (↑x : M) =
    f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), (↑x : M) ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) :=
  DFinsupp.mapRange (β₁ := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) (β₂ :=
    fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum' c))
    (fun (c : FiniteArchimedeanClass M) (x : ↥(seed.stratum c)) ↦
      Subtype.mk (p := fun (x : ↥seed.baseDomain) ↦ x ∈ seed.stratum' c)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseDomain) (↑x : M) ⋯) ⋯)
    ⋯ f
⊢ (↑((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c) : M) =
    (↑((seed.baseDomain.subtype.submoduleComap (seed.stratum c) :
            (a : ↥(Submodule.comap seed.baseDomain.subtype (seed.stratum c))) → ↥(seed.stratum c))
          ((f' : (a : FiniteArchimedeanClass M) → ↥(seed.stratum' a)) c)) :
      M)

Tactic:
simp [f']
-- 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
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h :
  (↑x : M) =
    f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), (↑x : M) ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) :=
  DFinsupp.mapRange (β₁ := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) (β₂ :=
    fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum' c))
    (fun (c : FiniteArchimedeanClass M) (x : ↥(seed.stratum c)) ↦
      Subtype.mk (p := fun (x : ↥seed.baseDomain) ↦ x ∈ seed.stratum' c)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseDomain) (↑x : M) ⋯) ⋯)
    ⋯ f
⊢ (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c =
    (seed.baseDomain.subtype.submoduleComap (seed.stratum c) :
        (a : ↥(Submodule.comap seed.baseDomain.subtype (seed.stratum c))) → ↥(seed.stratum c))
      ((f' : (a : FiniteArchimedeanClass M) → ↥(seed.stratum' a)) c)

Tactic:
have hf : f c = (seed.baseDomain.subtype.submoduleComap (seed.stratum c)) (f' c) := by
    apply Subtype.ext
    simp [f']
-- 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
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h :
  (↑x : M) =
    f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), (↑x : M) ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) :=
  DFinsupp.mapRange (β₁ := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) (β₂ :=
    fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum' c))
    (fun (c : FiniteArchimedeanClass M) (x : ↥(seed.stratum c)) ↦
      Subtype.mk (p := fun (x : ↥seed.baseDomain) ↦ x ∈ seed.stratum' c)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseDomain) (↑x : M) ⋯) ⋯)
    ⋯ f
hf :
  (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c =
    (seed.baseDomain.subtype.submoduleComap (seed.stratum c) :
        (a : ↥(Submodule.comap seed.baseDomain.subtype (seed.stratum c))) → ↥(seed.stratum c))
      ((f' : (a : FiniteArchimedeanClass M) → ↥(seed.stratum' a)) c)
change :
  x =
    (DirectSum.coeAddMonoidHom seed.stratum' :
        (a : ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) → ↥seed.baseDomain)
      f'
⊢ x =
    (Equiv.symm (decompose seed.stratum') :
        (a : ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) → ↥seed.baseDomain)
      f'

Tactic:
change x = f'.coeAddMonoidHom _

Premises used: DirectSum.coeAddMonoidHom, DFunLike.coe
-- 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
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h :
  (↑x : M) =
    f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), (↑x : M) ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) :=
  DFinsupp.mapRange (β₁ := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) (β₂ :=
    fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum' c))
    (fun (c : FiniteArchimedeanClass M) (x : ↥(seed.stratum c)) ↦
      Subtype.mk (p := fun (x : ↥seed.baseDomain) ↦ x ∈ seed.stratum' c)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseDomain) (↑x : M) ⋯) ⋯)
    ⋯ f
hf :
  (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c =
    (seed.baseDomain.subtype.submoduleComap (seed.stratum c) :
        (a : ↥(Submodule.comap seed.baseDomain.subtype (seed.stratum c))) → ↥(seed.stratum c))
      ((f' : (a : FiniteArchimedeanClass M) → ↥(seed.stratum' a)) c)
a :
  Eq (α := M) ((seed.baseDomain.subtype : (a : ↥seed.baseDomain) → M) x : M)
    ((seed.baseDomain.subtype : (a : ↥seed.baseDomain) → M)
        ((DirectSum.coeAddMonoidHom seed.stratum' :
              (a : ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) → ↥seed.baseDomain)
            f' :
          ↥seed.baseDomain) :
      M)
⊢ x =
    (DirectSum.coeAddMonoidHom seed.stratum' :
        (a : ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) → ↥seed.baseDomain)
      f'

Tactic:
apply Submodule.subtype_injective

Premises used: Submodule.subtype_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
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h :
  (↑x : M) =
    f.sum (β := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) fun (c : FiniteArchimedeanClass M) ↦
      (⇑(seed.stratum c).subtype : (a : ↥(seed.stratum c)) → M)
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), (↑x : M) ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) :=
  DFinsupp.mapRange (β₁ := fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum c)) (β₂ :=
    fun (c : FiniteArchimedeanClass M) ↦ ↥(seed.stratum' c))
    (fun (c : FiniteArchimedeanClass M) (x : ↥(seed.stratum c)) ↦
      Subtype.mk (p := fun (x : ↥seed.baseDomain) ↦ x ∈ seed.stratum' c)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ seed.baseDomain) (↑x : M) ⋯) ⋯)
    ⋯ f
hf :
  (f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) c =
    (seed.baseDomain.subtype.submoduleComap (seed.stratum c) :
        (a : ↥(Submodule.comap seed.baseDomain.subtype (seed.stratum c))) → ↥(seed.stratum c))
      ((f' : (a : FiniteArchimedeanClass M) → ↥(seed.stratum' a)) c)
⊢ ∀ (i : FiniteArchimedeanClass M), Eq.{u_2 + 1} (α := ↥seed.baseDomain) (↑0 : ↥seed.baseDomain) 0

Tactic:
simp