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

Goal state before:
pp: case pos
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : x = 0
⊢ min x.order y.order ≤ (x + y).order

pp: case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ min x.order y.order ≤ (x + y).order

Tactic:
·

Goal state after:
case pos
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : x = 0
⊢ min x.order y.order ≤ (x + y).order
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ min x.order y.order ≤ (x + y).order

pp: case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min x.order y.order ≤ (x + y).order

Tactic:
·

Goal state after:
case pos
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ min x.order y.order ≤ (x + y).order
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff

pp: case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff

Tactic:
·

Goal state after:
case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff

Tactic:
·

Goal state after:
case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case inl
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
hg : x.order ∈ y.support
⊢ x.order ∈ x.support

pp: case inr
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
⊢ g ∈ x.support

Tactic:
·

Goal state after:
case inl
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
hg : x.order ∈ y.support
⊢ x.order ∈ x.support
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case inr
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
⊢ g ∈ x.support

Tactic:
·

Goal state after:
case inr
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
⊢ g ∈ x.support
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
g : Γ'
hg : g ∈ Set.range ⇑f
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g

pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
g : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g

Tactic:
·

Goal state after:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
g : Γ'
hg : g ∈ Set.range ⇑f
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
g : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g

Tactic:
·

Goal state after:
case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
g : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : R⟦Γ⟧
hf : f = 0
⊢ (-f).order = f.order

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : R⟦Γ⟧
hf : ¬f = 0
⊢ (-f).order = f.order

Tactic:
·

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : R⟦Γ⟧
hf : f = 0
⊢ (-f).order = f.order
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
g : Γ'
hg : g ∈ Set.range ⇑f
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g

pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
g : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g

Tactic:
·

Goal state after:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
g : Γ'
hg : g ∈ Set.range ⇑f
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
g : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g

Tactic:
·

Goal state after:
case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
g : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab : a = b
⊢ a ≤ b ∨ b ≤ a

pp: case inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab : a ≠ b
⊢ a ≤ b ∨ b ≤ a

Tactic:
·

Goal state after:
case inl
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab : a = b
⊢ a ≤ b ∨ b ≤ a
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab : a ≠ b
⊢ a ≤ b ∨ b ≤ a

Tactic:
·

Goal state after:
case inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab : a ≠ b
⊢ a ≤ b ∨ b ≤ a
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.inl
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
hvu : v ⊆ u
hv : v.IsWF
i : Γ := hv.min hab
hji : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hne : (ofLex a).coeff i ≠ (ofLex b).coeff i
hi : (ofLex a).coeff i < (ofLex b).coeff i
⊢ a ≤ b ∨ b ≤ a

pp: case inr.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
hvu : v ⊆ u
hv : v.IsWF
i : Γ := hv.min hab
hji : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hne : (ofLex a).coeff i ≠ (ofLex b).coeff i
hi : (ofLex b).coeff i < (ofLex a).coeff i
⊢ a ≤ b ∨ b ≤ a

Tactic:
·

Goal state after:
case inr.inl
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
hvu : v ⊆ u
hv : v.IsWF
i : Γ := hv.min hab
hji : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hne : (ofLex a).coeff i ≠ (ofLex b).coeff i
hi : (ofLex a).coeff i < (ofLex b).coeff i
⊢ a ≤ b ∨ b ≤ a
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
hvu : v ⊆ u
hv : v.IsWF
i : Γ := hv.min hab
hji : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hne : (ofLex a).coeff i ≠ (ofLex b).coeff i
hi : (ofLex b).coeff i < (ofLex a).coeff i
⊢ a ≤ b ∨ b ≤ a

Tactic:
·

Goal state after:
case inr.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
hvu : v ⊆ u
hv : v.IsWF
i : Γ := hv.min hab
hji : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hne : (ofLex a).coeff i ≠ (ofLex b).coeff i
hi : (ofLex b).coeff i < (ofLex a).coeff i
⊢ a ≤ b ∨ b ≤ a
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mp
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
⊢ 0 < (ofLex x).leadingCoeff →
    ∃ i, (∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j) ∧ (ofLex 0).coeff i < (ofLex x).coeff i

pp: case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
⊢ (∃ i, (∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j) ∧ (ofLex 0).coeff i < (ofLex x).coeff i) →
    0 < (ofLex x).leadingCoeff

Tactic:
·

Goal state after:
case mp
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
⊢ 0 < (ofLex x).leadingCoeff →
    ∃ i, (∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j) ∧ (ofLex 0).coeff i < (ofLex x).coeff i
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
⊢ (∃ i, (∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j) ∧ (ofLex 0).coeff i < (ofLex x).coeff i) →
    0 < (ofLex x).leadingCoeff

Tactic:
·

Goal state after:
case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
⊢ (∃ i, (∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j) ∧ (ofLex 0).coeff i < (ofLex x).coeff i) →
    0 < (ofLex x).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case hg
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
⊢ i ∈ (ofLex x).support

pp: case hx
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
⊢ ∀ g' ∈ (ofLex x).support, i ≤ g'

Tactic:
·

Goal state after:
case hg
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
⊢ i ∈ (ofLex x).support
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case hx
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
⊢ ∀ g' ∈ (ofLex x).support, i ≤ g'

Tactic:
·

Goal state after:
case hx
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
⊢ ∀ g' ∈ (ofLex x).support, i ≤ g'
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mp
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ (ofLex x).leadingCoeff
⊢ 0 ≤ x

pp: case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ x
⊢ 0 ≤ (ofLex x).leadingCoeff

Tactic:
·

Goal state after:
case mp
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ (ofLex x).leadingCoeff
⊢ 0 ≤ x
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mp.inl
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ (ofLex x).leadingCoeff
heq : 0 = (ofLex x).leadingCoeff
⊢ 0 ≤ x

pp: case mp.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ (ofLex x).leadingCoeff
hlt : 0 < (ofLex x).leadingCoeff
⊢ 0 ≤ x

Tactic:
·

Goal state after:
case mp.inl
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ (ofLex x).leadingCoeff
heq : 0 = (ofLex x).leadingCoeff
⊢ 0 ≤ x
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mp.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ (ofLex x).leadingCoeff
hlt : 0 < (ofLex x).leadingCoeff
⊢ 0 ≤ x

Tactic:
·

Goal state after:
case mp.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ (ofLex x).leadingCoeff
hlt : 0 < (ofLex x).leadingCoeff
⊢ 0 ≤ x
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ x
⊢ 0 ≤ (ofLex x).leadingCoeff

Tactic:
·

Goal state after:
case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ x
⊢ 0 ≤ (ofLex x).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mpr.inl
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
h : 0 ≤ 0
⊢ 0 ≤ (ofLex 0).leadingCoeff

pp: case mpr.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ x
hlt : 0 < x
⊢ 0 ≤ (ofLex x).leadingCoeff

Tactic:
·

Goal state after:
case mpr.inl
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
h : 0 ≤ 0
⊢ 0 ≤ (ofLex 0).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mpr.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ x
hlt : 0 < x
⊢ 0 ≤ (ofLex x).leadingCoeff

Tactic:
·

Goal state after:
case mpr.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
h : 0 ≤ x
hlt : 0 < x
⊢ 0 ≤ (ofLex x).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : PartialOrder R
inst✝² : AddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
a c : Lex R⟦Γ⟧
hab : a ≤ a
⊢ a + c ≤ a + c

pp: case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : PartialOrder R
inst✝² : AddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
hlt : a < b
⊢ a + c ≤ b + c

Tactic:
·

Goal state after:
case inl
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : PartialOrder R
inst✝² : AddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
a c : Lex R⟦Γ⟧
hab : a ≤ a
⊢ a + c ≤ a + c
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : PartialOrder R
inst✝² : AddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
hlt : a < b
⊢ a + c ≤ b + c

Tactic:
·

Goal state after:
case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : PartialOrder R
inst✝² : AddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
hlt : a < b
⊢ a + c ≤ b + c
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 : Lex R⟦Γ⟧
hle : x ≤ 0
⊢ (ofLex |x|).support = (ofLex x).support

pp: case inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hge : 0 ≤ x
⊢ (ofLex |x|).support = (ofLex x).support

Tactic:
·

Goal state after:
case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hle : x ≤ 0
⊢ (ofLex |x|).support = (ofLex x).support
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hge : 0 ≤ x
⊢ (ofLex |x|).support = (ofLex x).support

Tactic:
·

Goal state after:
case inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hge : 0 ≤ x
⊢ (ofLex |x|).support = (ofLex x).support
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 : Lex R⟦Γ⟧
hle : x ≤ 0
⊢ (ofLex |x|).orderTop = (ofLex x).orderTop

pp: case inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hge : 0 ≤ x
⊢ (ofLex |x|).orderTop = (ofLex x).orderTop

Tactic:
·

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

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hge : 0 ≤ x
⊢ (ofLex |x|).orderTop = (ofLex x).orderTop

Tactic:
·

Goal state after:
case inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hge : 0 ≤ x
⊢ (ofLex |x|).orderTop = (ofLex x).orderTop
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
inst✝ : Zero Γ
⊢ (ofLex |0|).order = (ofLex 0).order

pp: case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : LinearOrder R
inst✝² : AddCommGroup R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
⊢ (ofLex |x|).order = (ofLex x).order

Tactic:
·

Goal state after:
case inl
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : LinearOrder R
inst✝² : AddCommGroup R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Zero Γ
⊢ (ofLex |0|).order = (ofLex 0).order
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : LinearOrder R
inst✝² : AddCommGroup R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
⊢ (ofLex |x|).order = (ofLex x).order

Tactic:
·

Goal state after:
case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : LinearOrder R
inst✝² : AddCommGroup R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
⊢ (ofLex |x|).order = (ofLex x).order
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 : Lex R⟦Γ⟧
hlt : x < 0
⊢ (ofLex |x|).leadingCoeff = |(ofLex x).leadingCoeff|

pp: case inr.inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
⊢ (ofLex |0|).leadingCoeff = |(ofLex 0).leadingCoeff|

pp: case inr.inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hgt : 0 < x
⊢ (ofLex |x|).leadingCoeff = |(ofLex x).leadingCoeff|

Tactic:
·

Goal state after:
case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hlt : x < 0
⊢ (ofLex |x|).leadingCoeff = |(ofLex x).leadingCoeff|
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case mp
M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c x : M
⊢ a * c ≤ x ∧ x < b * c → ∃ a_2, (a ≤ a_2 ∧ a_2 < b) ∧ a_2 * c = x

pp: case mpr
M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c x : M
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x) → a * c ≤ x ∧ x < b * c

Tactic:
·

Goal state after:
case mp
M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c x : M
⊢ a * c ≤ x ∧ x < b * c → ∃ a_2, (a ≤ a_2 ∧ a_2 < b) ∧ a_2 * c = 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
⊢ (ofLex |0|).leadingCoeff = |(ofLex 0).leadingCoeff|

pp: case inr.inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hgt : 0 < x
⊢ (ofLex |x|).leadingCoeff = |(ofLex x).leadingCoeff|

Tactic:
·

Goal state after:
case inr.inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
⊢ (ofLex |0|).leadingCoeff = |(ofLex 0).leadingCoeff|