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
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
refine_2 :
  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)
    (HahnSeries.coeff
        ((truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
            ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x)))
        d :
      R)
⊢ Eq.{u_3 + 1} (α := R)
    ((seed.coeff d : (a : ↥(seed.stratum d)) → R) ((f' : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) d) : R)
    (HahnSeries.coeff
        ((truncLTLinearMap K c : (a : R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
          ((ofLex : (a : Lex R⟦FiniteArchimedeanClass M⟧) → R⟦FiniteArchimedeanClass M⟧)
            ((↑seed.baseEmbedding : ↥seed.baseEmbedding.domain → Lex R⟦FiniteArchimedeanClass M⟧) x)))
        d :
      R)

Tactic:
unfold 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.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
refine_2 :
  (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
⊢ 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)
    ((seed.coeff d : (a : ↥(seed.stratum d)) → R) ((f : (a : FiniteArchimedeanClass M) → ↥(seed.stratum a)) d) : R)

Tactic:
apply congrArg

Premises used: congrArg
-- 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.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
⊢ ¬(↑c : ArchimedeanClass M) ≤ (↑d : ArchimedeanClass M)

Tactic:
have hcd : ¬ c.val ≤ d.val := not_le_of_gt hdc
-- 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.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)
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
⊢ (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

Tactic:
simp only [DFinsupp.mk_apply, hcd, ↓reduceIte]

Premises used: DFinsupp.mk_apply, reduceIte
-- 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.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)
⊢ (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:
aesop
-- 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.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
⊢ (↑c : ArchimedeanClass M) ≤ (↑d : ArchimedeanClass M)

Tactic:
have hcd : c.val ≤ d.val := hdc
-- 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.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)
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)
⊢ 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)

Tactic:
simp only [DFinsupp.mk_apply, hcd, ↓reduceIte]

Premises used: DFinsupp.mk_apply, reduceIte
-- 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.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) 0 : R) (0 : R)

Tactic:
LinearMap.map_zero _

Premises used: LinearMap.map_zero
-- 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.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)
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
⊢ 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:
convert! LinearMap.map_zero _

Premises used: LinearMap.map_zero
-- 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.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_2 + 1} (α := ↥(seed.stratum d))
    (if h : d ∈ f.support (β := fun (i : FiniteArchimedeanClass M) ↦ ↥(seed.stratum i)) then 0 else 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
f : Partial seed
⊢ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).toFun.toFun 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
f : Partial seed
x : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain
⊢ (f.toOrderAddMonoidHom :
        (a : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) → Lex R⟦FiniteArchimedeanClass M⟧)
      x =
    (↑(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧) :
        ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain → Lex R⟦FiniteArchimedeanClass M⟧)
      x

Tactic:
rfl

Premises used: rfl, LinearPMap.toFun'
-- 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
⊢ Function.Injective (α := ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) (β :=
    Lex (HahnSeries.{u_2, u_3} (FiniteArchimedeanClass M) R))
    (⇑f.toOrderAddMonoidHom :
      (a : ↥(↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain) → Lex R⟦FiniteArchimedeanClass M⟧)

Tactic:
f.prop.strictMono.injective

Premises used: Set.Mem, HahnEmbedding.IsPartial.strictMono, StrictMono.injective, Subtype.prop, LinearPMap.toFun'
-- 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 : M
c : FiniteArchimedeanClass M
hx : x ∈ seed.stratum c
apply : x ∈ (↑seed.baseEmbedding.domain : Set M)
⊢ x ∈ (↑f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧).domain

Tactic:
apply Set.mem_of_subset_of_mem f.prop.baseEmbedding_le.1

Premises used: HahnEmbedding.IsPartial.baseEmbedding_le, Set.mem_of_subset_of_mem, And.left, 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 : M
c : FiniteArchimedeanClass M
hx : x ∈ seed.stratum c
⊢ x ∈ (↑seed.baseEmbedding.domain : Set M)

Tactic:
apply seed.mem_domain_baseEmbedding hx

Premises used: HahnEmbedding.Seed.mem_domain_baseEmbedding