mathlib-initiative/mathlib-tactics huggingface dataset:
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
n : ℕ
hn :
  (ofLex y).orderTop ≤ (ofLex x).orderTop ∧
    ((ofLex x).orderTop = (ofLex y).orderTop → ∀ (n : ℕ), n • |(ofLex x).leadingCoeff| < |(ofLex y).leadingCoeff|)
⊢ |n • x| < |y|

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
n : ℕ
hn :
  (ofLex y).orderTop ≤ (ofLex x).orderTop ∧
    ((ofLex x).orderTop = (ofLex y).orderTop → ∀ (n : ℕ), n • |(ofLex x).leadingCoeff| < |(ofLex y).leadingCoeff|)
⊢ |n • x| < |y|
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⟦Γ⟧
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ∧ ArchimedeanClass.mk y ≤ ArchimedeanClass.mk x ↔
    (ofLex x).orderTop = (ofLex y).orderTop ∧
      ArchimedeanClass.mk (ofLex x).leadingCoeff = ArchimedeanClass.mk (ofLex y).leadingCoeff

Tactic:
archimedeanClassMk_le_archimedeanClassMk_iff,

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⟦Γ⟧
⊢ ((ofLex x).orderTop < (ofLex y).orderTop ∨
        (ofLex x).orderTop = (ofLex y).orderTop ∧
          ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff) ∧
      ArchimedeanClass.mk y ≤ ArchimedeanClass.mk x ↔
    (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: Γ : 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

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⟦Γ⟧
⊢ ((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.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
ι : Type u_2
x : α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ ⨆ i, x * f i = ⨆ i, x * f i

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
ι : Type u_2
x : α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ ⨆ i, f i * x = ⨆ i, f i * x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ ⨆ y_1 ∈ {y, z}, x * y_1 = ⨆ x_1 ∈ {y, z}, x * x_1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ ⨆ y_1 ∈ {x, y}, y_1 * z = ⨆ x_1 ∈ {x, y}, x_1 * z

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
a✝ : n₁✝ ≤ n₂✝
⊢ m✝ * n₂✝ = m✝ * n₂✝

pp: α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
a✝ : n₁✝ ≤ n₂✝
⊢ n₁✝ ≤ n₂✝

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
a✝ : n₁✝ ≤ n₂✝
⊢ n₁✝ ≤ n₂✝
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
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
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx : x ∈ ↑f.support
y : FiniteArchimedeanClass M
hy : y ∈ ↑f.support
hxy : x < y
⊢ ↑x < ArchimedeanClass.mk ↑(f 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
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
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx : x ∈ ↑f.support
y : FiniteArchimedeanClass M
hy : y ∈ ↑f.support
hxy : x < y
⊢ ↑x < ArchimedeanClass.mk ↑(f y)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝⁴ : Zero Γ
inst✝³ : PartialOrder Γ
inst✝² : Zero R
inst✝¹ : One R
inst✝ : NeZero 1
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
a✝ : n₁✝ ≤ n₂✝
⊢ swap (fun x1 x2 ↦ x1 * x2) m✝ n₂✝ = n₂✝ * m✝

pp: α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
a✝ : n₁✝ ≤ n₂✝
⊢ n₁✝ ≤ n₂✝

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
a✝ : n₁✝ ≤ n₂✝
⊢ n₁✝ ≤ n₂✝
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
a✝ : n₁✝ ≤ n₂✝
⊢ swap (fun x1 x2 ↦ x1 * x2) m✝ n₁✝ ≤ swap (fun x1 x2 ↦ x1 * x2) m✝ n₂✝

Tactic:
rwa [← left_eq_sup, ← sup_mul_distrib, sup_of_le_left]

Goal state after:
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
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
h1 : x ≤ y ⇨ₗ z
⊢ (y ⇨ₗ z) * y ≤ z

Tactic:
]

Goal state after:
α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
h1 : x ≤ y ⇨ₗ z
⊢ (y ⇨ₗ z) * y ≤ z
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✝¹ x✝ : { a // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h : FiniteArchimedeanClass.mk ↑⟨a, ha⟩ ⋯ ≤ FiniteArchimedeanClass.mk ↑⟨b, hb⟩ ⋯
⊢ (ofLex
          (match ⟨a, ha⟩ with
          | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).1 <
      (ofLex
          (match ⟨b, hb⟩ with
          | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).1 ∨
    (ofLex
            (match ⟨a, ha⟩ with
            | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).1 =
        (ofLex
            (match ⟨b, hb⟩ with
            | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).1 ∧
      (ofLex
            (match ⟨a, ha⟩ with
            | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).2 ≤
        (ofLex
            (match ⟨b, hb⟩ with
            | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).2

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x✝¹ x✝ : { a // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h : FiniteArchimedeanClass.mk ↑⟨a, ha⟩ ⋯ ≤ FiniteArchimedeanClass.mk ↑⟨b, hb⟩ ⋯
⊢ (ofLex
          (match ⟨a, ha⟩ with
          | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).1 <
      (ofLex
          (match ⟨b, hb⟩ with
          | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).1 ∨
    (ofLex
            (match ⟨a, ha⟩ with
            | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).1 =
        (ofLex
            (match ⟨b, hb⟩ with
            | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).1 ∧
      (ofLex
            (match ⟨a, ha⟩ with
            | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).2 ≤
        (ofLex
            (match ⟨b, hb⟩ with
            | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).2
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
h1 : x ≤ y ⇨ᵣ z
⊢ y * (y ⇨ᵣ z) ≤ z

Tactic:
]

Goal state after:
α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
h1 : x ≤ y ⇨ᵣ z
⊢ y * (y ⇨ᵣ z) ≤ z
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_3
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
x : α
⊢ ⨆ y ∈ ∅, y * x = sSup ∅

Tactic:
]

Goal state after:
α : Type u_3
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
x : α
⊢ ⨆ y ∈ ∅, y * x = sSup ∅
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_3
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
x : α
⊢ ⨆ y ∈ ∅, x * y = sSup ∅

Tactic:
]

Goal state after:
α : Type u_3
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
x : α
⊢ ⨆ y ∈ ∅, x * y = sSup ∅
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✝¹ x✝ : { a // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h : ArchimedeanClass.mk ↑⟨a, ha⟩ ≤ ArchimedeanClass.mk ↑⟨b, hb⟩
⊢ (ofLex a).orderTop.untop ⋯ < (ofLex b).orderTop.untop ⋯ ∨
    (ofLex a).orderTop.untop ⋯ = (ofLex b).orderTop.untop ⋯ ∧
      ArchimedeanClass.mk (ofLex a).leadingCoeff ≤ ArchimedeanClass.mk (ofLex b).leadingCoeff

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x✝¹ x✝ : { a // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h : ArchimedeanClass.mk ↑⟨a, ha⟩ ≤ ArchimedeanClass.mk ↑⟨b, hb⟩
⊢ (ofLex a).orderTop.untop ⋯ < (ofLex b).orderTop.untop ⋯ ∨
    (ofLex a).orderTop.untop ⋯ = (ofLex b).orderTop.untop ⋯ ∧
      ArchimedeanClass.mk (ofLex a).leadingCoeff ≤ ArchimedeanClass.mk (ofLex b).leadingCoeff
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✝¹ x✝ : { a // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h : ArchimedeanClass.mk ↑⟨a, ha⟩ ≤ ArchimedeanClass.mk ↑⟨b, hb⟩
⊢ (ofLex a).orderTop.untop ⋯ < (ofLex b).orderTop.untop ⋯ ∨
    (ofLex a).orderTop = ↑((ofLex b).orderTop.untop ⋯) ∧
      ArchimedeanClass.mk (ofLex a).leadingCoeff ≤ ArchimedeanClass.mk (ofLex b).leadingCoeff

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x✝¹ x✝ : { a // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h : ArchimedeanClass.mk ↑⟨a, ha⟩ ≤ ArchimedeanClass.mk ↑⟨b, hb⟩
⊢ (ofLex a).orderTop.untop ⋯ < (ofLex b).orderTop.untop ⋯ ∨
    (ofLex a).orderTop = ↑((ofLex b).orderTop.untop ⋯) ∧
      ArchimedeanClass.mk (ofLex a).leadingCoeff ≤ ArchimedeanClass.mk (ofLex b).leadingCoeff
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
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
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx : x ∈ ↑f.support
y : FiniteArchimedeanClass M
hy : y ∈ ↑f.support
hxy : x < y
⊢ ↑x < ↑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
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
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx : x ∈ ↑f.support
y : FiniteArchimedeanClass M
hy : y ∈ ↑f.support
hxy : x < y
⊢ ↑x < ↑y
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✝ : SMulZeroClass R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
⊢ ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2 =
    ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2

Tactic:
]

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✝ : SMulZeroClass R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
⊢ ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2 =
    ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2
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 : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ x✝ : { a // a ≠ 0 }
a : R
ha : a ≠ 0
b : R
hb : b ≠ 0
h : FiniteArchimedeanClass.mk ↑⟨a, ha⟩ ⋯ ≤ FiniteArchimedeanClass.mk ↑⟨b, hb⟩ ⋯
⊢ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑⟨a, ha⟩)) ⋯ ≤
    FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑⟨b, hb⟩)) ⋯

Tactic:
FiniteArchimedeanClass.mk_le_mk,

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ x✝ : { a // a ≠ 0 }
a : R
ha : a ≠ 0
b : R
hb : b ≠ 0
h : FiniteArchimedeanClass.mk ↑⟨a, ha⟩ ⋯ ≤ FiniteArchimedeanClass.mk ↑⟨b, hb⟩ ⋯
⊢ ArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑⟨a, ha⟩)) ≤
    ArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑⟨b, hb⟩))
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 : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ x✝ : { a // a ≠ 0 }
a : R
ha : a ≠ 0
b : R
hb : b ≠ 0
h : FiniteArchimedeanClass.mk ↑⟨a, ha⟩ ⋯ ≤ FiniteArchimedeanClass.mk ↑⟨b, hb⟩ ⋯
⊢ (ofLex (toLex ((single (ofLex x).1) ↑⟨a, ha⟩))).orderTop < (ofLex (toLex ((single (ofLex x).1) ↑⟨b, hb⟩))).orderTop ∨
    (ofLex (toLex ((single (ofLex x).1) ↑⟨a, ha⟩))).orderTop =
        (ofLex (toLex ((single (ofLex x).1) ↑⟨b, hb⟩))).orderTop ∧
      ArchimedeanClass.mk (ofLex (toLex ((single (ofLex x).1) ↑⟨a, ha⟩))).leadingCoeff ≤
        ArchimedeanClass.mk (ofLex (toLex ((single (ofLex x).1) ↑⟨b, hb⟩))).leadingCoeff

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ x✝ : { a // a ≠ 0 }
a : R
ha : a ≠ 0
b : R
hb : b ≠ 0
h : FiniteArchimedeanClass.mk ↑⟨a, ha⟩ ⋯ ≤ FiniteArchimedeanClass.mk ↑⟨b, hb⟩ ⋯
⊢ (ofLex (toLex ((single (ofLex x).1) ↑⟨a, ha⟩))).orderTop < (ofLex (toLex ((single (ofLex x).1) ↑⟨b, hb⟩))).orderTop ∨
    (ofLex (toLex ((single (ofLex x).1) ↑⟨a, ha⟩))).orderTop =
        (ofLex (toLex ((single (ofLex x).1) ↑⟨b, hb⟩))).orderTop ∧
      ArchimedeanClass.mk (ofLex (toLex ((single (ofLex x).1) ↑⟨a, ha⟩))).leadingCoeff ≤
        ArchimedeanClass.mk (ofLex (toLex ((single (ofLex x).1) ↑⟨b, hb⟩))).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✝ : SMulZeroClass R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : ((of R).symm y).support ⊆ s
b : Γ × Γ'
hb : (x.coeff b.1 ≠ 0 ∧ b.2 ∈ s ∧ b.1 +ᵥ b.2 = a) ∧ (x.coeff b.1 ≠ 0 → b.1 +ᵥ b.2 = a → ((of R).symm y).coeff b.2 = 0)
⊢ 0 = 0

Tactic:
]

Goal state after:
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✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.support ⊆ s
⊢ ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2 =
    ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2

Tactic:
]

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✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.support ⊆ s
⊢ ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2 =
    ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: 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
⊢ FiniteArchimedeanClass.mk (toLex ((single ao) a)) ⋯ ≤ FiniteArchimedeanClass.mk (toLex ((single bo) b)) ⋯

Tactic:
FiniteArchimedeanClass.mk_le_mk,

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
⊢ ArchimedeanClass.mk (toLex ((single ao) a)) ≤ ArchimedeanClass.mk (toLex ((single bo) b))
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
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk ↑(f i)) ↑f.support
⊢ f.support.min' hnonempty ≠ FiniteArchimedeanClass.mk a h0

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
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk ↑(f i)) ↑f.support
⊢ f.support.min' hnonempty ≠ FiniteArchimedeanClass.mk a h0