awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
    b
h0 : a ≠ 0
hnonempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).Nonempty
hmem :
  ∀ (x : FiniteArchimedeanClass M),
    (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) x) : M) ∈ u.stratum x
hmono :
  StrictMonoOn (β := ArchimedeanClass M)
    (fun (i : FiniteArchimedeanClass M) ↦
      ArchimedeanClass.mk (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M))
    (↑(f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))) :
      Set (FiniteArchimedeanClass M))
this_1 :
  f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)).min' hnonempty =
    FiniteArchimedeanClass.mk a h0
h : True
this : ArchimedeanClass.mk a = (↑c : ArchimedeanClass M)
⊢ FiniteArchimedeanClass.mk a h0 ∉ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
have this₁ : FiniteArchimedeanClass.mk a h0 = c
Tactic: rw [← val_mk h0, ← Subtype.ext_iff] at this
Cleared hypotheses: this
-- 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
    b
h0 : a ≠ 0
hnonempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)) = ∅
⊢ Ne (α := ArchimedeanClass M)
    (ArchimedeanClass.mk
      (∑ i ∈ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)),
        (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M)))
    (ArchimedeanClass.mk a)
have neg : Ne (α := ArchimedeanClass M)
  (ArchimedeanClass.mk (∑ i ∈ ∅, (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M)))
  (ArchimedeanClass.mk a)
Tactic: rw [hnonempty]
-- 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : Membership.mem (γ := Submodule K M) (⨆ (j : FiniteArchimedeanClass M), ⨆ (_ : j ≠ c), u.stratum j) b
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf :
  (f.sum (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i))
      fun (x : FiniteArchimedeanClass M) (xi : ↥(⨆ (_ : x ≠ c), u.stratum x)) ↦ (↑xi : M)) =
    b
h0 : a ≠ 0
hnonempty : f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(⨆ (_ : i ≠ c), u.stratum i)) = ∅
⊢ Ne (α := ArchimedeanClass M)
    (ArchimedeanClass.mk (∑ i ∈ ∅, (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M)))
    (ArchimedeanClass.mk a)
have neg : Ne (α := ArchimedeanClass M) (ArchimedeanClass.mk a)
  (ArchimedeanClass.mk (∑ i ∈ ∅, (↑((f : (a : FiniteArchimedeanClass M) → ↥(⨆ (_ : a ≠ c), u.stratum a)) i) : M)))
Tactic: symm
-- 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
u : ArchimedeanStrata K M
⊢ iSupIndep u.stratum'
have apply : iSupIndep (α := (↑(Set.Iic u.baseDomain) : Type u_2))
  ((⇑u.baseDomain.mapIic : (a : Submodule K ↥u.baseDomain) → (↑(Set.Iic u.baseDomain) : Type u_2)) ∘ u.stratum')
Tactic: apply (iSupIndep_map_orderIso_iff (Submodule.mapIic u.baseDomain)).mp
-- 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
u : ArchimedeanStrata K M
⊢ iSupIndep (α := (↑(Set.Iic u.baseDomain) : Type u_2))
    ((⇑u.baseDomain.mapIic : (a : Submodule K ↥u.baseDomain) → (↑(Set.Iic u.baseDomain) : Type u_2)) ∘ u.stratum')
have ht : iSupIndep (α := Submodule K M)
  (Function.comp (β := (↑(Set.Iic u.baseDomain) : Type u_2))
    (Subtype.val (p := fun (x : Submodule K M) ↦ x ∈ Set.Iic u.baseDomain))
    ((⇑u.baseDomain.mapIic : (a : Submodule K ↥u.baseDomain) → (↑(Set.Iic u.baseDomain) : Type u_2)) ∘ u.stratum'))
Tactic: apply iSupIndep.of_coe_Iic_comp
-- 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
u : ArchimedeanStrata K M
⊢ iSupIndep (α := Submodule K M)
    (Function.comp (β := (↑(Set.Iic u.baseDomain) : Type u_2))
      (Subtype.val (p := fun (x : Submodule K M) ↦ x ∈ Set.Iic u.baseDomain))
      ((⇑u.baseDomain.mapIic : (a : Submodule K ↥u.baseDomain) → (↑(Set.Iic u.baseDomain) : Type u_2)) ∘ u.stratum'))
have h : Function.comp (β := (↑(Set.Iic u.baseDomain) : Type u_2))
    (Subtype.val (p := fun (x : Submodule K M) ↦ x ∈ Set.Iic u.baseDomain))
    ((⇑u.baseDomain.mapIic : (a : Submodule K ↥u.baseDomain) → (↑(Set.Iic u.baseDomain) : Type u_2)) ∘ u.stratum') =
  u.stratum
Tactic: convert! u.iSupIndep_stratum
-- 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
u : ArchimedeanStrata K M
⊢ Function.comp (β := (↑(Set.Iic u.baseDomain) : Type u_2))
      (Subtype.val (p := fun (x : Submodule K M) ↦ x ∈ Set.Iic u.baseDomain))
      ((⇑u.baseDomain.mapIic : (a : Submodule K ↥u.baseDomain) → (↑(Set.Iic u.baseDomain) : Type u_2)) ∘ u.stratum') =
    u.stratum
have h : ∀ (c : FiniteArchimedeanClass M),
  Function.comp (β := (↑(Set.Iic u.baseDomain) : Type u_2))
      (Subtype.val (p := fun (x : Submodule K M) ↦ x ∈ Set.Iic u.baseDomain))
      ((⇑u.baseDomain.mapIic : (a : Submodule K ↥u.baseDomain) → (↑(Set.Iic u.baseDomain) : Type u_2)) ∘ u.stratum') c =
    u.stratum c
Tactic: ext1 c
-- 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
u : ArchimedeanStrata K M
⊢ IsInternal u.stratum'
have apply : iSup u.stratum' = ⊤
Tactic: apply DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top u.iSupIndep_stratum'
-- 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
u : ArchimedeanStrata K M
⊢ iSup u.stratum' = ⊤
have a : Submodule.map u.baseDomain.subtype (iSup u.stratum') = Submodule.map u.baseDomain.subtype ⊤
Tactic: apply Submodule.map_injective_of_injective u.baseDomain.subtype_injective
-- 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
u : ArchimedeanStrata K M
⊢ Submodule.map u.baseDomain.subtype (iSup u.stratum') = Submodule.map u.baseDomain.subtype ⊤
have a : ⨆ (i : FiniteArchimedeanClass M), u.baseDomain ⊓ u.stratum i = u.baseDomain
Tactic: suffices ⨆ i, u.baseDomain ⊓ u.stratum i = u.baseDomain by simpa using this
-- 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
u : ArchimedeanStrata K M
⊢ ⨆ (i : FiniteArchimedeanClass M), u.baseDomain ⊓ u.stratum i = u.baseDomain
have a : ∀ (i : FiniteArchimedeanClass M), u.baseDomain ⊓ u.stratum i = u.stratum i
Tactic: apply iSup_congr
-- 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.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
⊢ (((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)
have 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
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]
-- 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_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)
⊢ (↑x : M) ∈ seed.baseDomain
have apply : (↑(seed.stratum c) : Set M) ⊆ (↑seed.baseDomain : Set M)
Tactic: apply Set.mem_of_mem_of_subset x.prop
-- 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.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
⊢ (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
have hxm : ∀ {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 _ _
-- 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.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)
have 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)
Tactic: apply Subtype.ext
-- 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.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
⊢ (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
have 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)
Tactic: have hf : f c = (seed.baseDomain.subtype.submoduleComap (seed.stratum c)) (f' c) := by
    apply Subtype.ext
    simp [f']
-- 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.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)
⊢ x =
    (Equiv.symm (decompose seed.stratum') :
        (a : ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) → ↥seed.baseDomain)
      f'
have change : x =
  (DirectSum.coeAddMonoidHom seed.stratum' :
      (a : ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) → ↥seed.baseDomain)
    f'
Tactic: change x = f'.coeAddMonoidHom _
-- 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.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)
⊢ x =
    (DirectSum.coeAddMonoidHom seed.stratum' :
        (a : ⨁ (i : FiniteArchimedeanClass M), ↥(seed.stratum' i)) → ↥seed.baseDomain)
      f'
have 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)
Tactic: apply Submodule.subtype_injective