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

Goal state before:
pp: case inr.mp
Γ : 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 = (ofLex ((n + 1) • |x|)).coeff j_1
hi : (ofLex |y|).coeff j < (ofLex ((n + 1) • |x|)).coeff j
⊢ |(ofLex y).leadingCoeff| ≤ (n + 1) • |(ofLex x).leadingCoeff|

Tactic:
[

Goal state after:
case inr.mp
Γ : 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 = (ofLex ((n + 1) • |x|)).coeff j_1
hi : (ofLex |y|).coeff j < (ofLex ((n + 1) • |x|)).coeff j
⊢ |(ofLex y).leadingCoeff| ≤ (n + 1) • |(ofLex x).leadingCoeff|
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.mp
Γ : 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).leadingCoeff| ≤ (n + 1) • |(ofLex x).leadingCoeff|

Tactic:
[

Goal state after:
case inr.mp
Γ : 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).leadingCoeff| ≤ (n + 1) • |(ofLex x).leadingCoeff|
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.mp
Γ : 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|).coeff ((ofLex |y|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)

Tactic:
[

Goal state after:
case inr.mp
Γ : 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|).coeff ((ofLex |y|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)
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|).coeff ((ofLex x).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex x).orderTop.untop ⋯)

Tactic:
[

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|
⊢ (ofLex |y|).coeff ((ofLex x).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex x).orderTop.untop ⋯)
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.inr
Γ : 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
⊢ 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:
[

Goal state after:
case inr.inr
Γ : 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
⊢ 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
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : DistribSMul R V
x : R⟦Γ⟧
y z : HahnModule Γ' R V
k b : Γ'
h : ((of R).symm y).coeff b = 0 ∧ ((of R).symm z).coeff b = 0
⊢ 0 + ((of R).symm z).coeff b = 0

Tactic:
h.2,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : DistribSMul R V
x : R⟦Γ⟧
y z : HahnModule Γ' R V
k b : Γ'
h : ((of R).symm y).coeff b = 0 ∧ ((of R).symm z).coeff b = 0
⊢ 0 + 0 = 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⟦Γ⟧
⊢ { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } a ≤
      { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } b ↔
    a ≤ b

Tactic:
[

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⟦Γ⟧
⊢ { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } a ≤
      { toFun := fun a ↦ toLex (embDomain f (ofLex a)), inj' := ⋯ } b ↔
    a ≤ b
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.baseEmbedding.domain
⊢ 0 < ↑seed.baseEmbedding x

Tactic:
[

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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseEmbedding.domain
⊢ 0 < ↑seed.baseEmbedding x
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case neg
Γ : 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
k : Γ'
hki : k < f i
hkmem : k ∉ Set.range ⇑f
⊢ (embDomain f (ofLex a)).coeff k = (embDomain f (ofLex b)).coeff k

Tactic:
[

Goal state after:
case neg
Γ : 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
k : Γ'
hki : k < f i
hkmem : k ∉ Set.range ⇑f
⊢ (embDomain f (ofLex a)).coeff k = (embDomain f (ofLex b)).coeff k
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case e'_3
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm : |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| ≤ m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)|
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|
⊢ |ArchimedeanOrder.val (ArchimedeanOrder.of (x₂ * y₂))| =
    |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| * |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)|

Tactic:
[

Goal state after:
case e'_3
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm : |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| ≤ m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)|
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|
⊢ |ArchimedeanOrder.val (ArchimedeanOrder.of (x₂ * y₂))| =
    |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| * |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)|
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case e'_4
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm : |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| ≤ m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)|
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|
⊢ (m * n) • |ArchimedeanOrder.val (ArchimedeanOrder.of (x₁ * y₁))| =
    m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)| * n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|

Tactic:
[

Goal state after:
case e'_4
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm : |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| ≤ m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)|
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|
⊢ (m * n) • |ArchimedeanOrder.val (ArchimedeanOrder.of (x₁ * y₁))| =
    m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)| * n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case succ
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y : R
h : mk x = mk y
n : ℕ
IH : mk (x ^ n) = mk (y ^ n)
⊢ mk (x ^ (n + 1)) = mk (y ^ (n + 1))

Tactic:
[

Goal state after:
case succ
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y : R
h : mk x = mk y
n : ℕ
IH : mk (x ^ n) = mk (y ^ n)
⊢ mk (x ^ (n + 1)) = mk (y ^ (n + 1))
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk.mk.mk
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y z : R
⊢ mk x + mk y + mk z = mk x + (mk y + mk z)

Tactic:
[

Goal state after:
case mk.mk.mk
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y z : R
⊢ mk x + mk y + mk z = mk x + (mk y + mk z)
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:
[

Goal state after:
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
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
  rw [← smul_eq_mul]
  exact HahnModule.orderTop_vAdd_le_orderTop_smul fun i j ↦ rfl

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
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h✝ : Nontrivial R
⊢ ((single g) r).leadingCoeff * x.leadingCoeff ≠ 0

Tactic:
leadingCoeff_of_single,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h✝ : Nontrivial R
⊢ r * x.leadingCoeff ≠ 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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseEmbedding.domain
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))) ∈ seed.baseEmbedding.toFun.range

Tactic:
[

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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseEmbedding.domain
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))) ∈ seed.baseEmbedding.toFun.range
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✝ : NonUnitalCommSemiring R
x y : R⟦Γ⟧
x✝ : Γ
⊢ (x * y).coeff x✝ = (y * x).coeff x✝

Tactic:
[

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✝ : NonUnitalCommSemiring R
x y : R⟦Γ⟧
x✝ : Γ
⊢ (x * y).coeff x✝ = (y * x).coeff x✝
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case mpr
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
h : x.orderTop = 0 ∧ x.leadingCoeff = 1
⊢ x.leadingCoeff = leadingCoeff 1

Tactic:
h.2,

Goal state after:
case mpr
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
h : x.orderTop = 0 ∧ x.leadingCoeff = 1
⊢ 1 = leadingCoeff 1
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
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧ˣ
hx : (↑x).orderTop = 0 ∧ (↑x).leadingCoeff = 1
hy : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
h✝ : Nontrivial R
⊢ 1 * (↑y).leadingCoeff = 1

Tactic:
hy.2,

Goal state after:
Γ✝ : 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
x y : R⟦Γ⟧ˣ
hx : (↑x).orderTop = 0 ∧ (↑x).leadingCoeff = 1
hy : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
h✝ : Nontrivial R
⊢ 1 * 1 = 1
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ∀ x_1 ∈ antidiagonal ⋯ ⋯ x, ((single a) r).coeff x_1.1 * ((single b) s).coeff x_1.2 = 0

Tactic:
[

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ∀ x_1 ∈ antidiagonal ⋯ ⋯ x, ((single a) r).coeff x_1.1 * ((single b) s).coeff x_1.2 = 0
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x✝¹ : P.IsOrdering
a b : R
x✝ : -(a * b) ∈ P
this✝ : ¬(a ∈ P ∨ b ∈ P)
this : a * b ∈ P
⊢ a * b ∈ P.support

Tactic:
by simp_all [mem_support]

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
f : Partial seed
inst✝ : IsOrderedAddMonoid R
x y : ↥(↑f).domain
⊢ ArchimedeanClass.mk (↑↑f x) = ArchimedeanClass.mk (↑↑f y) ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y

Tactic:
[

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
f : Partial seed
inst✝ : IsOrderedAddMonoid R
x y : ↥(↑f).domain
⊢ ArchimedeanClass.mk (↑↑f x) = ArchimedeanClass.mk (↑↑f y) ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y
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
f : Partial seed
inst✝ : IsOrderedAddMonoid R
x y : ↥(↑f).domain
⊢ ArchimedeanClass.mk x = ArchimedeanClass.mk y ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y

Tactic:
[

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
f : Partial seed
inst✝ : IsOrderedAddMonoid R
x y : ↥(↑f).domain
⊢ ArchimedeanClass.mk x = ArchimedeanClass.mk y ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case inr
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x y : ↥(↑f).domain
hnontrivial : Nontrivial M
hnonempty : Nonempty (FiniteArchimedeanClass M)
c : FiniteArchimedeanClass M
this : Nontrivial R
⊢ (ofLex (↑↑f x)).orderTop = (ofLex (↑↑f y)).orderTop ↔ ArchimedeanClass.mk (↑↑f x) = ArchimedeanClass.mk (↑↑f y)

Tactic:
[

Goal state after:
case inr
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x y : ↥(↑f).domain
hnontrivial : Nontrivial M
hnonempty : Nonempty (FiniteArchimedeanClass M)
c : FiniteArchimedeanClass M
this : Nontrivial R
⊢ (ofLex (↑↑f x)).orderTop = (ofLex (↑↑f y)).orderTop ↔ ArchimedeanClass.mk (↑↑f x) = ArchimedeanClass.mk (↑↑f y)
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
y z : ↥(↑f).domain
c : FiniteArchimedeanClass M
hy : ↑y - x ∈ ball K c
hz : ↑z - x ∈ ball K c
d : FiniteArchimedeanClass M
hd : d ≤ c
this : ↑(y - z) = ↑y - x - (↑z - x)
⊢ ↑(y - z) ∈ ball K c

Tactic:
this

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
y z : ↥(↑f).domain
c : FiniteArchimedeanClass M
hy : ↑y - x ∈ ball K c
hz : ↑z - x ∈ ball K c
d : FiniteArchimedeanClass M
hd : d ≤ c
this : ↑(y - z) = ↑y - x - (↑z - x)
⊢ ↑y - x - (↑z - x) ∈ ball K c
Module: Mathlib.Algebra.Order.Star.Conjneg

Goal state before:
pp: G : Type u_1
R : Type u_2
inst✝⁴ : AddGroup G
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
f : G → R
⊢ 0 < conjneg f ↔ 0 < f

Tactic:
[

Goal state after:
G : Type u_1
R : Type u_2
inst✝⁴ : AddGroup G
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
f : G → R
⊢ 0 < conjneg f ↔ 0 < f
Module: Mathlib.Algebra.Order.Star.Conjneg

Goal state before:
pp: G : Type u_1
R : Type u_2
inst✝⁴ : AddGroup G
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
f : G → R
⊢ conjneg f ≤ 0 ↔ f ≤ 0

Tactic:
[

Goal state after:
G : Type u_1
R : Type u_2
inst✝⁴ : AddGroup G
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
f : G → R
⊢ conjneg f ≤ 0 ↔ f ≤ 0
Module: Mathlib.Algebra.Order.Star.Conjneg

Goal state before:
pp: G : Type u_1
R : Type u_2
inst✝⁴ : AddGroup G
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
f : G → R
⊢ conjneg f < 0 ↔ f < 0

Tactic:
[

Goal state after:
G : Type u_1
R : Type u_2
inst✝⁴ : AddGroup G
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
f : G → R
⊢ conjneg f < 0 ↔ f < 0