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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst✝² : CommRing α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hf_na : IsNonarchimedean ⇑f
s : Multiset α
m : ℕ
g : Multiset α → α := fun t ↦ t.prod
b : Multiset α
hb_in : powersetCard (s.card - m) s ≠ 0 → b ∈ powersetCard (s.card - m) s
hb_le : f (map g (powersetCard (s.card - m) s)).sum ≤ f (g b)
⊢ b ≤ s ∧ b.card = s.card - m

Tactic:
by

Goal state after:
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 : R
hx : 0 < mk x
y : S
hy : 0 < y
⊢ x < f y

Tactic:
by

Goal state after:
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⟦Γ⟧
⊢ (x + y) * z = x * z + y * z

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst✝² : CommRing α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hf_na : IsNonarchimedean ⇑f
s : Multiset α
m : ℕ
⊢ ∃ t, t.card = s.card - m ∧ (∀ x ∈ t, x ∈ s) ∧ f (map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
β : Type u_4
inst✝² : CommRing α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hf_na : IsNonarchimedean ⇑f
s : Finset β
b : β → α
m : ℕ
g : Finset β → α := fun t ↦ ∏ i ∈ t, -b i
⊢ f 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
β : Type u_4
inst✝² : CommRing α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hf_na : IsNonarchimedean ⇑f
s : Finset β
b : β → α
m : ℕ
⊢ ∃ u, f (∑ t ∈ powersetCard (#s - m) s, ∏ i ∈ t, -b i) ≤ f (∏ i ∈ ↑u, -b i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
⊢ ((single b) r * x).coeff (a + b) = r * x.coeff a

Tactic:
by

Goal state after:
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 : R
hx : 0 < mk x
y : S
hy : y < 0
⊢ f y < x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
hcard : ¬s.card = 1
⊢ 1 < s.card

Tactic:
by

Goal state after:
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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk ↑(f x)) ↑f.support
hsupport' : (f.support.erase (f.support.min' hsupport)).Nonempty
⊢ ↑(f.support.erase (f.support.min' hsupport)) ⊆ ↑f.support

Tactic:
by

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
hcard : ¬s.card = 1
⊢ f (l k + ∑ x ∈ s.erase k, l x) = f (l k)

Tactic:
have hNonempty : (s.erase k).Nonempty :=
      Finset.Nontrivial.erase_nonempty (Finset.one_lt_card_iff_nontrivial.mp (by grind))

Goal state after:
case neg
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
hcard : ¬s.card = 1
hNonempty : (s.erase k).Nonempty
⊢ f (l k + ∑ x ∈ s.erase k, l x) = f (l k)
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: S : Type u_3
inst✝² : LinearOrder S
inst✝¹ : CommRing S
inst✝ : IsStrictOrderedRing S
n : ℤ
h : n ≠ 0
h✝ : Nontrivial S
x✝ : ℤ
⊢ ∀ ⦃b : ℤ⦄, x✝ ≤ b → (↑↑(Int.castRingHom S)).toFun x✝ ≤ (↑↑(Int.castRingHom S)).toFun b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
hcard : ¬s.card = 1
hNonempty : (s.erase k).Nonempty
hrest_le : ∃ b, (¬b = k ∧ b ∈ s) ∧ f (∑ i ∈ s.erase k, l i) ≤ f (l b)
⊢ f (l k) ≠ f (∑ x ∈ s.erase k, l x)

Tactic:
by

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

Goal state before:
pp: S : Type u_3
inst✝² : LinearOrder S
inst✝¹ : CommRing S
inst✝ : IsStrictOrderedRing S
n : ℤ
h : n ≠ 0
⊢ mk ↑n = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
hcard : ¬s.card = 1
hNonempty : (s.erase k).Nonempty
hrest_le : ∃ b, (¬b = k ∧ b ∈ s) ∧ f (∑ i ∈ s.erase k, l i) ≤ f (l b)
⊢ f (∑ x ∈ s.erase k, l x) < f (l k)

Tactic:
by

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

Goal state before:
pp: S : Type u_3
inst✝² : LinearOrder S
inst✝¹ : CommRing S
inst✝ : IsStrictOrderedRing S
n : ℤ
⊢ 0 ≤ mk ↑n

Tactic:
by

Goal state after:
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
hx : 0 ≤ mk x
⊢ ∃ n, x ≤ ↑n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
⊢ f (∑ i ∈ s, l i) = f (l k)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
⊢ f 0 = 0

Tactic:
by

Goal state after:
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
hx : 0 ≤ mk x
⊢ ∃ n, x < ↑n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
⊢ ∀ (x : α), 0 ≤ f x

Tactic:
by

Goal state after:
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
hx : 0 ≤ mk x
⊢ ∃ n, x ≤ ↑n

Tactic:
obtain ⟨n, hn⟩ := exists_nat_ge_of_mk_nonneg hx
  exact ⟨n, mod_cast hn⟩

Goal state after:
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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk ↑(f x)) ↑f.support
hsupport' : (f.support.erase (f.support.min' hsupport)).Nonempty
⊢ ↑(f ((f.support.erase (f.support.min' hsupport)).min' hsupport')) ≠ 0

Tactic:
by

Goal state after:
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
hx : 0 ≤ mk x
⊢ ∃ n, ↑n ≤ x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
⊢ ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Tactic:
by

Goal state after:
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
hx : 0 ≤ mk x
⊢ ∃ n, ↑n < x

Tactic:
by

Goal state after:
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 : R
r s : S
hr : f r ≤ x
hs : x ≤ f s
⊢ 0 ≤ mk x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y z : ArchimedeanClass R
hx : x ≠ ⊤
h : x + y = x + z
⊢ y = z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p q : RingPreordering R
h : (fun P ↦ (↑P).carrier) p = (fun P ↦ (↑P).carrier) q
⊢ p = q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x : R
⊢ x * x ∈ P

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x : R
⊢ x ^ 2 ∈ P

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
A B : RingPreordering R
h : ↑A = ↑B
⊢ A = B

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
S : Set R
hS : S = ↑P
a✝ b✝ : R
ha : a✝ ∈ S
hb : b✝ ∈ S
⊢ a✝ * b✝ ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
S : Set R
hS : S = ↑P
⊢ 1 ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
S : Set R
hS : S = ↑P
a✝ b✝ : R
ha : a✝ ∈ S
hb : b✝ ∈ S
⊢ a✝ + b✝ ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
S : Set R
hS : S = ↑P
⊢ 0 ∈ S

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y z : ArchimedeanClass R
hx : x ≠ ⊤
h : y + x = z + x
⊢ y = z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
⊢ ∀ {a b : R}, a ∈ ↑P ∩ -↑P → b ∈ ↑P ∩ -↑P → a + b ∈ ↑P ∩ -↑P

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
⊢ 0 ∈ ↑P ∩ -↑P

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
⊢ ∀ {x : R}, x ∈ ↑P ∩ -↑P → -x ∈ ↑P ∩ -↑P

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
⊢ (x * (single b) r).coeff (a + b) = x.coeff a * r

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
⊢ (x * (single 0) r).coeff a = x.coeff a * r

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
⊢ ((single 0) r * x).coeff a = r * x.coeff a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
r : R
x : R⟦Γ⟧
⊢ (single 0) r * x = r • x

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ (x * y).support ⊆ x.support + y.support

Tactic:
by

Goal state after:
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✝ : R⟦Γ⟧
⊢ 0 * x✝ = 0

Tactic:
by

Goal state after:
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✝ : R⟦Γ⟧
⊢ x✝ * 0 = 0

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ (x * y).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).coeff (x.order + y.order) ≠ 0

Tactic:
by

Goal state after:
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
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
⊢ 0 ≤ f 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h✝ : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
h : x * y = 0
⊢ False

Tactic:
by

Goal state after:
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
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
⊢ 0 ≤ f (n • q)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
by

Goal state after:
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
⊢ mk x ≤ mk y ↔ ∃ q, 0 < f q ∧ f q * |y| ≤ |x|

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: case inr.inr
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⁻¹ = mk y⁻¹

Tactic:
have hx' : mk x ≠ ⊤ := by simpa using hx

Goal state after:
case inr.inr
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
hx' : mk x ≠ ⊤
⊢ mk x⁻¹ = mk y⁻¹
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
⊢ mk x⁻¹ = mk y⁻¹

Tactic:
by

Goal state after:
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
n : ℤ
x y : R
h : mk x = mk y
⊢ mk (x ^ n) = mk (y ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst✝ : NoZeroDivisors R
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ x.orderTop + y.orderTop ≤ (x * y).orderTop

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
⊢ x.leadingCoeff ≠ 0

Tactic:
by

Goal state after: