mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
⊢ 0 < |x|

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
⊢ ¬x = 0
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
a b : G
hab : a ≤ b
ha : a ≤ 0
hb : b ≤ 0
⊢ ¬0 < a + b

Tactic:
simpa using

Goal state after:
M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
a b : G
hab : a ≤ b
ha : a ≤ 0
hb : b ≤ 0
⊢ a + b ≤ 0
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
a b : G
hab : a ≤ (fun x ↦ a + x) b
⊢ 0 ≤ b

Tactic:
simpa using

Goal state after:
M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
a b : G
hab : a ≤ (fun x ↦ a + x) b
⊢ 0 ≤ b
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
⊢ ofLex |y| ≠ 0

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
⊢ ¬y = 0
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
⊢ ofLex |x| ≠ 0

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
⊢ ¬x = 0
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulLeftMono M
u : Mˣ
x✝¹ x✝ : M
h : ↑u * x✝¹ ≤ ↑u * x✝
⊢ x✝¹ ≤ x✝

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulLeftMono M
u : Mˣ
x✝¹ x✝ : M
h : ↑u * x✝¹ ≤ ↑u * x✝
⊢ x✝¹ ≤ x✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulRightMono M
a b : M
u : Mˣ
x✝ : a * ↑u ≤ b * ↑u
⊢ a ≤ b

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulRightMono M
a b : M
u : Mˣ
x✝ : a * ↑u ≤ b * ↑u
⊢ a ≤ b
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
⊢ (ofLex x).orderTop ≠ ⊤

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
⊢ ¬x = 0
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
j : Γ
hj : j < (ofLex x).orderTop.untop ⋯
⊢ ↑j < (ofLex |y|).orderTop

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
j : Γ
hj : j < (ofLex x).orderTop.untop ⋯
⊢ ↑j < (ofLex x).orderTop
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
j : Γ
hj : j < (ofLex x).orderTop.untop ⋯
⊢ ↑j < (ofLex |x|).orderTop

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
j : Γ
hj : j < (ofLex x).orderTop.untop ⋯
⊢ ↑j < (ofLex x).orderTop
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
this : (ofLex |y|).leadingCoeff < (n + 1) • (ofLex |x|).leadingCoeff
⊢ ofLex |y| ≠ 0

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
this : (ofLex |y|).leadingCoeff < (n + 1) • (ofLex |x|).leadingCoeff
⊢ ¬y = 0
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
this : (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).leadingCoeff
⊢ ofLex |x| ≠ 0

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
this : (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).leadingCoeff
⊢ ¬x = 0
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
eq : u.stratum c = ⊥
⊢ ball K c ⊔ ⊥ < closedBall K c

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
eq : u.stratum c = ⊥
⊢ ball K c < closedBall K c
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
⊢ ↑a ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
⊢ ¬a = 0
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
⊢ ↑b ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
⊢ ¬b = 0
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hlt : (ofLex x).orderTop < (ofLex y).orderTop
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    (ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧
        ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff

Tactic:
simpa using

Goal state after:
case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hlt : (ofLex x).orderTop < (ofLex y).orderTop
⊢ ∃ n, |y| ≤ n • |x|
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hlt : (ofLex x).orderTop < (ofLex y).orderTop
⊢ |y| ≤ 1 • |x|

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hlt : (ofLex x).orderTop < (ofLex y).orderTop
⊢ |y| ≤ |x|
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
heq : (ofLex x).orderTop = (ofLex y).orderTop
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    (ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧
        ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff

Tactic:
simpa using

Goal state after:
case inr.inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
heq : (ofLex x).orderTop = (ofLex y).orderTop
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hgt : (ofLex y).orderTop < (ofLex x).orderTop
n : ℕ
hn :
  (ofLex y).orderTop ≤ (ofLex x).orderTop ∧
    ((ofLex x).orderTop = (ofLex y).orderTop → ∀ (n : ℕ), n • |(ofLex x).leadingCoeff| < |(ofLex y).leadingCoeff|)
⊢ (ofLex x).orderTop ≤ (ofLex (n • x)).orderTop

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hgt : (ofLex y).orderTop < (ofLex x).orderTop
n : ℕ
hn :
  (ofLex y).orderTop ≤ (ofLex x).orderTop ∧
    ((ofLex x).orderTop = (ofLex y).orderTop → ∀ (n : ℕ), n • |(ofLex x).leadingCoeff| < |(ofLex y).leadingCoeff|)
⊢ (ofLex x).orderTop ≤ (n • ofLex x).orderTop
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mp
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
⊢ ((ofLex x).orderTop < (ofLex y).orderTop ∨
        (ofLex x).orderTop = (ofLex y).orderTop ∧
          ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff) ∧
      ((ofLex y).orderTop < (ofLex x).orderTop ∨
        (ofLex y).orderTop = (ofLex x).orderTop ∧
          ArchimedeanClass.mk (ofLex y).leadingCoeff ≤ ArchimedeanClass.mk (ofLex x).leadingCoeff) →
    (ofLex x).orderTop = (ofLex y).orderTop ∧
      ArchimedeanClass.mk (ofLex x).leadingCoeff = ArchimedeanClass.mk (ofLex y).leadingCoeff

Tactic:
simpa using

Goal state after:
case mp
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
⊢ (ofLex x).orderTop = (ofLex y).orderTop →
    ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff →
      ArchimedeanClass.mk (ofLex y).leadingCoeff ≤ ArchimedeanClass.mk (ofLex x).leadingCoeff →
        ArchimedeanClass.mk (ofLex x).leadingCoeff = ArchimedeanClass.mk (ofLex y).leadingCoeff
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx : x ∈ ↑f.support
y : FiniteArchimedeanClass M
hy : y ∈ ↑f.support
hxy : x < y
⊢ ↑(f x) ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx : x ∈ ↑f.support
y : FiniteArchimedeanClass M
hy : y ∈ ↑f.support
hxy : x < y
⊢ ¬f x = 0
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx : x ∈ ↑f.support
y : FiniteArchimedeanClass M
hy : y ∈ ↑f.support
hxy : x < y
⊢ ↑(f y) ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx : x ∈ ↑f.support
y : FiniteArchimedeanClass M
hy : y ∈ ↑f.support
hxy : x < y
⊢ ¬f y = 0
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x✝¹ x✝ : { a // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h : ArchimedeanClass.mk ↑⟨a, ha⟩ ≤ ArchimedeanClass.mk ↑⟨b, hb⟩
⊢ (ofLex a).orderTop.untop ⋯ < (ofLex b).orderTop.untop ⋯ ∨
    (ofLex a).orderTop = ↑((ofLex b).orderTop.untop ⋯) ∧
      ArchimedeanClass.mk (ofLex a).leadingCoeff ≤ ArchimedeanClass.mk (ofLex b).leadingCoeff

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x✝¹ x✝ : { a // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h : ArchimedeanClass.mk ↑⟨a, ha⟩ ≤ ArchimedeanClass.mk ↑⟨b, hb⟩
⊢ (ofLex a).orderTop < (ofLex b).orderTop ∨
    (ofLex a).orderTop = (ofLex b).orderTop ∧
      ArchimedeanClass.mk (ofLex a).leadingCoeff ≤ ArchimedeanClass.mk (ofLex b).leadingCoeff
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk ↑(f i)) ↑f.support
⊢ ↑(f (f.support.min' hnonempty)) ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk ↑(f i)) ↑f.support
⊢ ¬f (f.support.min' hnonempty) = 0
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case pos
K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk ↑(f i)) ↑f.support
this✝ : f.support.min' hnonempty = FiniteArchimedeanClass.mk a h0
h : True
this : FiniteArchimedeanClass.mk a h0 = c
⊢ FiniteArchimedeanClass.mk a h0 ∉ f.support

Tactic:
simpa using

Goal state after:
case pos
K : Type u_1
inst✝⁸ : DivisionRing K
inst✝⁷ : LinearOrder K
inst✝⁶ : IsOrderedRing K
inst✝⁵ : Archimedean K
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module K M
inst✝ : IsOrderedModule K M
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk ↑(f i)) ↑f.support
this✝ : f.support.min' hnonempty = FiniteArchimedeanClass.mk a h0
h : True
this : FiniteArchimedeanClass.mk a h0 = c
⊢ f c = 0