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

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

Tactic:
·

Goal state after:
case inr.mp.inr.inr
Γ : 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
hjgt : (ofLex |x|).orderTop < ↑j
⊢ (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.mpr
Γ : 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, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|) → ∃ n, |y| ≤ n • |x|

Tactic:
·

Goal state after:
case inr.mpr
Γ : 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, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|) → ∃ n, |y| ≤ n • |x|
Module: Mathlib.RingTheory.HahnSeries.Lex

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

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

Tactic:
·

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

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

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

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|
j : Γ
hj : j < (ofLex x).orderTop.untop ⋯
⊢ (ofLex |y|).coeff j = 0
Module: Mathlib.RingTheory.HahnSeries.Lex

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

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|
j : Γ
hj : j < (ofLex x).orderTop.untop ⋯
⊢ 0 = (ofLex ((n + 1) • |x|)).coeff j
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case a
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
h0 : a ≠ 0
⊢ ArchimedeanClass.mk a ≤ ↑c

pp: case a
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
h0 : a ≠ 0
⊢ ↑c ≤ ArchimedeanClass.mk a

Tactic:
·

Goal state after:
case a
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
h0 : a ≠ 0
⊢ ArchimedeanClass.mk a ≤ ↑c
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case a
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
h0 : a ≠ 0
⊢ ↑c ≤ ArchimedeanClass.mk a

Tactic:
·

Goal state after:
case a
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
h0 : a ≠ 0
⊢ ↑c ≤ ArchimedeanClass.mk a
Module: Mathlib.RingTheory.HahnSeries.Lex

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

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

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 inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
hlt : (ofLex x).orderTop < (ofLex y).orderTop
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    (ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧
        ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Lex

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

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.inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
heq : (ofLex x).orderTop = (ofLex y).orderTop
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    (ofLex x).orderTop < (ofLex y).orderTop ∨
      (ofLex x).orderTop = (ofLex y).orderTop ∧
        ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

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

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 (∑ i ∈ f.support, ↑(f i)) ≠ ArchimedeanClass.mk a

Tactic:
·

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

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

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
case mpr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
⊢ (ofLex x).orderTop = (ofLex y).orderTop ∧
      ArchimedeanClass.mk (ofLex x).leadingCoeff = ArchimedeanClass.mk (ofLex y).leadingCoeff →
    ((ofLex x).orderTop < (ofLex y).orderTop ∨
        (ofLex x).orderTop = (ofLex y).orderTop ∧
          ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff) ∧
      ((ofLex y).orderTop < (ofLex x).orderTop ∨
        (ofLex y).orderTop = (ofLex x).orderTop ∧
          ArchimedeanClass.mk (ofLex y).leadingCoeff ≤ ArchimedeanClass.mk (ofLex x).leadingCoeff)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_3
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : MulZeroOneClass R
h✝ : Subsingleton R
⊢ order 1 = 0

pp: case inr
Γ : Type u_1
R : Type u_3
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : MulZeroOneClass R
h✝ : Nontrivial R
⊢ order 1 = 0

Tactic:
·

Goal state after:
case inl
Γ : Type u_1
R : Type u_3
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : MulZeroOneClass R
h✝ : Subsingleton R
⊢ order 1 = 0
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : MulZeroOneClass R
h✝ : Nontrivial R
⊢ order 1 = 0

Tactic:
·

Goal state after:
case inr
Γ : Type u_1
R : Type u_3
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : MulZeroOneClass R
h✝ : Nontrivial R
⊢ order 1 = 0
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a b : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
ac : FiniteArchimedeanClass R
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
bc : FiniteArchimedeanClass R
h✝ : toLex (ao, ac) ≤ toLex (bo, bc)
h : (ofLex (toLex (ao, ac))).1 < (ofLex (toLex (bo, bc))).1
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, ac)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (bo, bc))

pp: case inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a b : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
ac : FiniteArchimedeanClass R
x✝ : Γ × FiniteArchimedeanClass R
bc : FiniteArchimedeanClass R
h : toLex (ao, ac) ≤ toLex ((ofLex (toLex (ao, ac))).1, bc)
hle : (ofLex (toLex (ao, ac))).2 ≤ (ofLex (toLex ((ofLex (toLex (ao, ac))).1, bc))).2
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, ac)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex ((ofLex (toLex (ao, ac))).1, bc))

Tactic:
·

Goal state after:
case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a b : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
ac : FiniteArchimedeanClass R
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
bc : FiniteArchimedeanClass R
h✝ : toLex (ao, ac) ≤ toLex (bo, bc)
h : (ofLex (toLex (ao, ac))).1 < (ofLex (toLex (bo, bc))).1
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, ac)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (bo, bc))
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inl.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a✝ b : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
bc : FiniteArchimedeanClass R
a : R
ha : a ≠ 0
h✝ : toLex (ao, FiniteArchimedeanClass.mk a ha) ≤ toLex (bo, bc)
h : (ofLex (toLex (ao, FiniteArchimedeanClass.mk a ha))).1 < (ofLex (toLex (bo, bc))).1
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, FiniteArchimedeanClass.mk a ha)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (bo, bc))

Tactic:
induction bc using FiniteArchimedeanClass.ind with | mk b hb
       =>  _ 

Goal state after:
case inl.mk.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a✝ b✝ : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
a : R
ha : a ≠ 0
b : R
hb : b ≠ 0
h✝ : toLex (ao, FiniteArchimedeanClass.mk a ha) ≤ toLex (bo, FiniteArchimedeanClass.mk b hb)
h : (ofLex (toLex (ao, FiniteArchimedeanClass.mk a ha))).1 < (ofLex (toLex (bo, FiniteArchimedeanClass.mk b hb))).1
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, FiniteArchimedeanClass.mk a ha)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (bo, FiniteArchimedeanClass.mk b hb))
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
a b : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
ac : FiniteArchimedeanClass R
x✝ : Γ × FiniteArchimedeanClass R
bc : FiniteArchimedeanClass R
h : toLex (ao, ac) ≤ toLex ((ofLex (toLex (ao, ac))).1, bc)
hle : (ofLex (toLex (ao, ac))).2 ≤ (ofLex (toLex ((ofLex (toLex (ao, ac))).1, bc))).2
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, ac)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex ((ofLex (toLex (ao, ac))).1, bc))

Tactic:
·

Goal state after:
case inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a b : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
ac : FiniteArchimedeanClass R
x✝ : Γ × FiniteArchimedeanClass R
bc : FiniteArchimedeanClass R
h : toLex (ao, ac) ≤ toLex ((ofLex (toLex (ao, ac))).1, bc)
hle : (ofLex (toLex (ao, ac))).2 ≤ (ofLex (toLex ((ofLex (toLex (ao, ac))).1, bc))).2
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, ac)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex ((ofLex (toLex (ao, ac))).1, bc))