mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case neg
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 = ∅
⊢ ArchimedeanClass.mk a ≠ ArchimedeanClass.mk (∑ i ∈ ∅, ↑(f i))

Tactic:
simpa using

Goal state after:
case neg
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 = ∅
⊢ ¬a = 0
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
k : Γ
hj : ∀ j < f k, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex b)).coeff j
hi : (embDomain f (ofLex a)).coeff (f k) < (embDomain f (ofLex b)).coeff (f k)
⊢ (ofLex a).coeff k < (ofLex b).coeff k

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
k : Γ
hj : ∀ j < f k, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex b)).coeff j
hi : (embDomain f (ofLex a)).coeff (f k) < (embDomain f (ofLex b)).coeff (f k)
⊢ (ofLex a).coeff k < (ofLex b).coeff k
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mp.inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
k : Γ
hj : ∀ j < f k, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex b)).coeff j
hi : (embDomain f (ofLex a)).coeff (f k) < (embDomain f (ofLex b)).coeff (f k)
j : Γ
hjk : j < k
⊢ (ofLex a).coeff j = (ofLex b).coeff j

Tactic:
simpa using

Goal state after:
case mp.inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
k : Γ
hj : ∀ j < f k, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex b)).coeff j
hi : (embDomain f (ofLex a)).coeff (f k) < (embDomain f (ofLex b)).coeff (f k)
j : Γ
hjk : j < k
⊢ (ofLex a).coeff j = (ofLex b).coeff j
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hi : (ofLex a).coeff i < (ofLex b).coeff i
⊢ (embDomain f (ofLex a)).coeff (f i) < (embDomain f (ofLex b)).coeff (f i)

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hi : (ofLex a).coeff i < (ofLex b).coeff i
⊢ (ofLex a).coeff i < (ofLex b).coeff i
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hi : (ofLex a).coeff i < (ofLex b).coeff i
j' : Γ
hki : f j' < f i
⊢ (embDomain f (ofLex a)).coeff (f j') = (embDomain f (ofLex b)).coeff (f j')

Tactic:
simpa using

Goal state after:
case pos
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hi : (ofLex a).coeff i < (ofLex b).coeff i
j' : Γ
hki : f j' < f i
⊢ (ofLex a).coeff j' = (ofLex b).coeff j'
Module: Mathlib.Algebra.Order.Ring.Cone

Goal state before:
pp: T : Type u_1
inst✝² : Ring T
inst✝¹ : PartialOrder T
inst✝ : IsOrderedRing T
a✝ a : T
⊢ a ∈ (Subsemiring.nonneg T).carrier → -a ∈ (Subsemiring.nonneg T).carrier → a = 0

Tactic:
simpa using

Goal state after:
T : Type u_1
inst✝² : Ring T
inst✝¹ : PartialOrder T
inst✝ : IsOrderedRing T
a✝ a : T
⊢ 0 ≤ a → a ≤ 0 → a = 0
Module: Mathlib.Algebra.Order.Ring.Cone

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : SetLike S R
C : S
inst✝ : RingConeClass S R
x✝ : PartialOrder R := PartialOrder.mkOfAddGroupCone C
this✝ : IsOrderedAddMonoid R
this : ZeroLEOneClass R
x y : R
xnn : 0 ≤ x
ynn : 0 ≤ y
⊢ x * y - 0 ∈ C

Tactic:
simpa using

Goal state after:
S : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : SetLike S R
C : S
inst✝ : RingConeClass S R
x✝ : PartialOrder R := PartialOrder.mkOfAddGroupCone C
this✝ : IsOrderedAddMonoid R
this : ZeroLEOneClass R
x y : R
xnn : 0 ≤ x
ynn : 0 ≤ y
⊢ x * y ∈ C
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case inr
α : Type u_2
S : Type u_3
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
fna : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
H : ∀ {a b : α}, f a ≠ f b → f a > f b → f (a + b) = max (f a) (f b)
hab : ¬f a > f b
⊢ f (a + b) = max (f a) (f b)

Tactic:
simpa using

Goal state after:
case inr
α : Type u_2
S : Type u_3
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
fna : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
H : ∀ {a b : α}, f a ≠ f b → f a > f b → f (a + b) = max (f a) (f b)
hab : ¬f a > f b
⊢ f (a + b) = max (f a) (f b)
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case inl
α : Type u_2
S : Type u_3
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
fna : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
h : f (a + b + -b) ≤ f (a + b)
⊢ max (f a) (f b) ≤ f (a + b)

Tactic:
simpa using

Goal state after:
case inl
α : Type u_2
S : Type u_3
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
fna : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
h : f (a + b + -b) ≤ f (a + b)
⊢ f a ≤ f (a + b)
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: α : Type u_2
S : Type u_3
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
fna : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
h : f (a + b + -b) ≤ f (-b)
⊢ f (-b) < f (a + b + -b)

Tactic:
simpa using

Goal state after:
α : Type u_2
S : Type u_3
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
fna : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
h : f (a + b + -b) ≤ f (-b)
⊢ f (-b) < f a
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ 0
y z : R
hyz : (fun x_1 ↦ mk x + x_1) (mk y) = (fun x_1 ↦ mk x + x_1) (mk z)
⊢ mk y = mk z

Tactic:
simpa using

Goal state after:
case mk.mk
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ 0
y z : R
hyz : (fun x_1 ↦ mk x + x_1) (mk y) = (fun x_1 ↦ mk x + x_1) (mk z)
⊢ (∃ m, |z| ≤ ↑m * |y|) ∧ ∃ n, |y| ≤ ↑n * |z|
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : S
h : x ≠ 0
⊢ mk (f x) = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : S
h : x ≠ 0
⊢ mk (f x) = 0
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : α → R
hna : IsNonarchimedean f
g : β → α
t : Finset β
ht : t.Nonempty
⊢ ∃ b ∈ t, f (t.sum g) ≤ f (g b)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : α → R
hna : IsNonarchimedean f
g : β → α
t : Finset β
ht : t.Nonempty
⊢ ∃ b ∈ t, f (t.sum g) ≤ f (g b)
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
y : S
⊢ 0 ≤ mk (f y)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
y : S
⊢ 0 ≤ mk (f y)
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case hpos
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : R
hx : 0 < mk x
y : S
hy : 0 < y
⊢ 0 ≤ f y

Tactic:
simpa using

Goal state after:
case hpos
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : R
hx : 0 < mk x
y : S
hy : 0 < y
⊢ 0 ≤ f y
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
⊢ (HahnModule.of R).symm ((x + y) • (HahnModule.of R) z) =
    (HahnModule.of R).symm (x • (HahnModule.of R) z) + (HahnModule.of R).symm (y • (HahnModule.of R) z)

Tactic:
refine HahnModule.add_smul ?_

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
⊢ ∀ (r s u : R), (r + s) • u = r • u + s • u
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case hneg
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : R
hx : 0 < mk x
y : S
hy : y < 0
⊢ f y ≤ 0

Tactic:
simpa using

Goal state after:
case hneg
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : R
hx : 0 < mk x
y : S
hy : y < 0
⊢ f y ≤ 0
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of x)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of 1)|
⊢ |x| ≤ ↑n

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of x)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of 1)|
⊢ |x| ≤ ↑n
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
q : R
⊢ 0 < f q ↔ 0 < q

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
q : R
⊢ 0 < f q ↔ 0 < q
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x✝ : P.HasIdealSupport
⊢ ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x✝ : P.HasIdealSupport
⊢ ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ' : Type u_2
R : Type u_3
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : PartialOrder Γ'
inst✝¹ : AddCommGroup Γ'
inst✝ : IsOrderedAddMonoid Γ'
r : R
x : R⟦Γ'⟧
a b : Γ'
⊢ ((single b) r * x).coeff a = r * x.coeff (a - b)

Tactic:
simpa using

Goal state after:
Γ' : Type u_2
R : Type u_3
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : PartialOrder Γ'
inst✝¹ : AddCommGroup Γ'
inst✝ : IsOrderedAddMonoid Γ'
r : R
x : R⟦Γ'⟧
a b : Γ'
⊢ ((single b) r * x).coeff a = r * x.coeff (a - b)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ' : Type u_2
R : Type u_3
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : PartialOrder Γ'
inst✝¹ : AddCommGroup Γ'
inst✝ : IsOrderedAddMonoid Γ'
r : R
x : R⟦Γ'⟧
a b : Γ'
⊢ (x * (single b) r).coeff a = x.coeff (a - b) * r

Tactic:
simpa using

Goal state after:
Γ' : Type u_2
R : Type u_3
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : PartialOrder Γ'
inst✝¹ : AddCommGroup Γ'
inst✝ : IsOrderedAddMonoid Γ'
r : R
x : R⟦Γ'⟧
a b : Γ'
⊢ (x * (single b) r).coeff a = x.coeff (a - b) * r
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : HasMemOrNegMem P
x a : R
ha : a ∈ P.supportAddSubgroup
hx : x ∈ P
⊢ x * a ∈ ↑P

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : HasMemOrNegMem P
x a : R
ha : a ∈ P.supportAddSubgroup
hx : x ∈ P
⊢ x * a ∈ P
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : HasMemOrNegMem P
x a : R
ha : a ∈ P.supportAddSubgroup
hx : x ∈ P
⊢ x * a ∈ -↑P

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : HasMemOrNegMem P
x a : R
ha : a ∈ P.supportAddSubgroup
hx : x ∈ P
⊢ -(x * a) ∈ P
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : HasMemOrNegMem P
x a : R
ha : a ∈ P.supportAddSubgroup
hx : -x ∈ P
⊢ x * a ∈ ↑P

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : HasMemOrNegMem P
x a : R
ha : a ∈ P.supportAddSubgroup
hx : -x ∈ P
⊢ x * a ∈ P
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : HasMemOrNegMem P
x a : R
ha : a ∈ P.supportAddSubgroup
hx : -x ∈ P
⊢ x * a ∈ -↑P

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : HasMemOrNegMem P
x a : R
ha : a ∈ P.supportAddSubgroup
hx : -x ∈ P
⊢ -(x * a) ∈ P
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : P.HasIdealSupport
⊢ ∀ (c : R) {x : R}, x ∈ P.supportAddSubgroup.carrier → c • x ∈ P.supportAddSubgroup.carrier

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : P.HasIdealSupport
⊢ ∀ (c : R) {x : R}, x ∈ P.supportAddSubgroup → c * x ∈ P.supportAddSubgroup
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mp.succ
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y)| ≤ (n + 1) • |ArchimedeanOrder.val (ArchimedeanOrder.of x)|
q : R
hq₀ : 0 < q
hq : (n + 1) • q < 1
⊢ (↑n + 1) * (f q * |y|) ≤ (↑n + 1) * |x|

Tactic:
simpa using

Goal state after:
case mp.succ
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y)| ≤ (n + 1) • |ArchimedeanOrder.val (ArchimedeanOrder.of x)|
q : R
hq₀ : 0 < q
hq : (n + 1) • q < 1
⊢ (↑n + 1) * f q * |y| ≤ (↑n + 1) * |x|
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
q : R
hq₀ : 0 < f q
hq : f q * |y| ≤ |x|
hq₀' : 0 < q
n : ℕ
hn : 1 < n • q
h : 0 ≤ f (n • q)
⊢ f q * |ArchimedeanOrder.val (ArchimedeanOrder.of y)| ≤ f q * n • |ArchimedeanOrder.val (ArchimedeanOrder.of x)|

Tactic:
simpa using

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
q : R
hq₀ : 0 < f q
hq : f q * |y| ≤ |x|
hq₀' : 0 < q
n : ℕ
hn : 1 < n • q
h : 0 ≤ f (n • q)
⊢ f q * |y| ≤ f q * (↑n * |x|)
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
h : mk x = mk y
hx : x ≠ 0
hy : y ≠ 0
⊢ mk x ≠ ⊤

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
h : mk x = mk y
hx : x ≠ 0
hy : y ≠ 0
⊢ ¬x = 0
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
q : ℚ
h : q ≠ 0
⊢ mk ↑q = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
q : ℚ
h : q ≠ 0
⊢ mk ↑q = 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
seed : Seed K M R
inst✝ : IsOrderedAddMonoid R
x y : ↥seed.baseEmbedding.domain
h : x < y
⊢ 0 < y - x

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
seed : Seed K M R
inst✝ : IsOrderedAddMonoid R
x y : ↥seed.baseEmbedding.domain
h : x < y
⊢ x < y
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
q : ℚ
h : q ≠ 0
⊢ mk ↑q = 0

Tactic:
by
  simpa using mk_map_of_archimedean ⟨(Rat.castHom R).toAddMonoidHom, fun _ ↦ by simp⟩ h

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
⊢ mk x ≤ mk y ↔ ∃ q, 0 < q ∧ ↑q * |y| ≤ |x|

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
⊢ mk x ≤ mk y ↔ ∃ q, 0 < q ∧ ↑q * |y| ≤ |x|
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case inr.refine_1
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Nontrivial R
this : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
nz : (↑y).leadingCoeff * y.inv.leadingCoeff ≠ 0
⊢ y.inv.orderTop = 0

Tactic:
simpa using

Goal state after:
case inr.refine_1
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Nontrivial R
this : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
nz : (↑y).leadingCoeff * y.inv.leadingCoeff ≠ 0
⊢ (↑y⁻¹).orderTop = 0
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case inr.refine_2
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Nontrivial R
this : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
nz : (↑y).leadingCoeff * y.inv.leadingCoeff ≠ 0
⊢ y.inv.leadingCoeff = 1

Tactic:
simpa using

Goal state after:
case inr.refine_2
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Nontrivial R
this : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
nz : (↑y).leadingCoeff * y.inv.leadingCoeff ≠ 0
⊢ (↑y⁻¹).leadingCoeff = 1
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R✝¹ : Type u_1
inst✝² : CommRing R✝¹
P✝¹ : RingPreordering R✝¹
R✝ : Type u_2
inst✝¹ : CommRing R✝
P✝ : Set R✝
add✝ : ?m.2
mul✝ : ?m.3
sq✝ : ?m.4
neg_one✝ : ?m.5
R : Type u_3
inst✝ : CommRing R
P : Set R
add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P
mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P
sq : ∀ (x : R), x * x ∈ P
neg_one : -1 ∉ P
x y : R
⊢ x ∈ P → y ∈ P → x * y ∈ P

Tactic:
simpa using

Goal state after:
R✝¹ : Type u_1
inst✝² : CommRing R✝¹
P✝¹ : RingPreordering R✝¹
R✝ : Type u_2
inst✝¹ : CommRing R✝
P✝ : Set R✝
add✝ : ?m.2
mul✝ : ?m.3
sq✝ : ?m.4
neg_one✝ : ?m.5
R : Type u_3
inst✝ : CommRing R
P : Set R
add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P
mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P
sq : ∀ (x : R), x * x ∈ P
neg_one : -1 ∉ P
x y : R
⊢ x ∈ P → y ∈ P → x * y ∈ P
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R✝¹ : Type u_1
inst✝² : CommRing R✝¹
P✝¹ : RingPreordering R✝¹
R✝ : Type u_2
inst✝¹ : CommRing R✝
P✝ : Set R✝
add✝ : ?m.2
mul✝ : ?m.3
sq✝ : ?m.4
neg_one✝ : ?m.5
R : Type u_3
inst✝ : CommRing R
P : Set R
add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P
mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P
sq : ∀ (x : R), x * x ∈ P
neg_one : -1 ∉ P
⊢ 1 ∈ P

Tactic:
simpa using

Goal state after:
R✝¹ : Type u_1
inst✝² : CommRing R✝¹
P✝¹ : RingPreordering R✝¹
R✝ : Type u_2
inst✝¹ : CommRing R✝
P✝ : Set R✝
add✝ : ?m.2
mul✝ : ?m.3
sq✝ : ?m.4
neg_one✝ : ?m.5
R : Type u_3
inst✝ : CommRing R
P : Set R
add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P
mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P
sq : ∀ (x : R), x * x ∈ P
neg_one : -1 ∉ P
⊢ 1 ∈ P