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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
⊢ ¬x = 0 ↔ x ≠ 0

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Lex (Γ × Γ')⟧
h₁ :
  (Function.support fun g ↦ { coeff := fun g' ↦ x.coeff (g, g'), isPWO_support' := ⋯ }) =
    Function.support fun g g' ↦ x.coeff (g, g')
⊢ (Prod.fst '' Function.support x.coeff).IsPWO

Tactic:
]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Lex (Γ × Γ')⟧
h₁ :
  (Function.support fun g ↦ { coeff := fun g' ↦ x.coeff (g, g'), isPWO_support' := ⋯ }) =
    Function.support fun g g' ↦ x.coeff (g, g')
⊢ (Prod.fst '' Function.support x.coeff).IsPWO
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
x : α
hx : ∀ i ∈ S, x ∈ ↑i
⊢ False

Tactic:
]

Goal state after:
case neg.inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
x : α
hx : ∀ i ∈ S, x ∈ ↑i
⊢ False
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r s : R
rs : (single a) r = (single a) s
⊢ ((single a) s).coeff a = ((single a) s).coeff a

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : PartialOrder Γ
inst✝² : Zero R
a b : Γ
r✝ : R
inst✝¹ : Nonempty Γ
inst✝ : Nontrivial R
r s : R
rs : r ≠ s
inhabited_h : Inhabited Γ
con : (single default) r = (single default) s
⊢ s = s

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
g : Γ
hg : g ∈ x.support
hx : ∀ g' ∈ x.support, g ≤ g'
⊢ ↑g = ↑g

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
g : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min ⋯ = g
⊢ x.coeff g ≠ 0

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
g : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min ⋯ = g
⊢ x.coeff g ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
g : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min ⋯ = g
⊢ x.coeff (⋯.min ⋯) ≠ 0

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
g : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min ⋯ = g
⊢ x.coeff (⋯.min ⋯) ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Zero R
Γ : Type u_5
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
g : Γ
h : x.coeff g ≠ 0
⊢ ⋯.min ⋯ ≤ g

Tactic:
]

Goal state after:
R : Type u_3
inst✝¹ : Zero R
Γ : Type u_5
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
g : Γ
h : x.coeff g ≠ 0
⊢ ⋯.min ⋯ ≤ g
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
hr : ¬r = 0
⊢ ↑a ≤ ↑a

Tactic:
]

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

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬↑i < x.orderTop

Tactic:
]

Goal state after:
case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬↑i < x.orderTop
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min ⋯

Tactic:
]

Goal state after:
case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min ⋯
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
hx✝ : x.orderTop ≠ ⊤
hx : x ≠ 0
⊢ x.coeff (x.orderTop.untop hx✝) = x.leadingCoeff

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
hx✝ : x.orderTop ≠ ⊤
hx : x ≠ 0
⊢ x.coeff (x.orderTop.untop hx✝) = x.leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
hx✝ : x.orderTop ≠ ⊤
hx : x ≠ 0
⊢ x.coeff (⋯.min ⋯) = x.coeff (⋯.min ⋯)

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
x : R⟦Γ⟧
inst✝ : Zero Γ
hx : x ≠ 0
⊢ ↑(⋯.min ⋯) = ↑(⋯.min ⋯)

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : ¬x = 0
⊢ ¬x.coeff (⋯.min ⋯) = 0

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : ¬x = 0
⊢ ¬x.coeff (⋯.min ⋯) = 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < x.order

Tactic:
]

Goal state after:
case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < x.order
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min ⋯

Tactic:
]

Goal state after:
case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min ⋯
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
h : x = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b✝ : Γ
r : R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
b : Γ'
hb : b ∉ ⇑f '' x.support
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
⊢ { coeff := fun b ↦ if h : b ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0, isPWO_support' := ⋯ }.coeff
      (f a) =
    x.coeff a

Tactic:
]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
⊢ { coeff := fun b ↦ if h : b ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0, isPWO_support' := ⋯ }.coeff
      (f a) =
    x.coeff a
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∈ x.support
⊢ x.coeff (Classical.choose ⋯) = x.coeff a

Tactic:
]

Goal state after:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∈ x.support
⊢ x.coeff (Classical.choose ⋯) = x.coeff a
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∉ x.support
⊢ 0 = 0

pp: case neg.hnc
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∉ x.support
⊢ f a ∉ ⇑f '' x.support

Tactic:
]

Goal state after:
case neg.hnc
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∉ x.support
⊢ f a ∉ ⇑f '' x.support
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case neg.hnc
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : f a ∈ ⇑f '' x.support
b : Γ
hb1 : a ∈ x.support
hb2 : f b = f a
⊢ a ∈ x.support

Tactic:
]

Goal state after:
case neg.hnc
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : f a ∈ ⇑f '' x.support
b : Γ
hb1 : a ∈ x.support
hb2 : f b = f a
⊢ a ∈ x.support
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
g : Γ'
hg : g ∉ ⇑f '' x.support
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = f g
⊢ 0 = 0

pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = f g
⊢ g' ∉ ⇑f '' ((single g) r).support

Tactic:
]

Goal state after:
case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = f g
⊢ g' ∉ ⇑f '' ((single g) r).support
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = f g
hr : ¬r = 0
⊢ ¬g' = f g

Tactic:
]

Goal state after:
case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = f g
hr : ¬r = 0
⊢ ¬g' = f g
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
⊢ x.coeff g = y.coeff g

Tactic:
]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
⊢ x.coeff g = y.coeff g
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
xyg : x.coeff g = y.coeff g
⊢ x.coeff g = y.coeff g

Tactic:
]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
xyg : x.coeff g = y.coeff g
⊢ x.coeff g = y.coeff g
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : V⟦Γ⟧
hrx : r • x = 0
⊢ ¬⊤ < x.orderTop

Tactic:
]

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : V⟦Γ⟧
hrx : r • x = 0
⊢ ¬⊤ < x.orderTop
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inr
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
⊢ (embDomain f x).orderTop = ↑(f (x.orderTop.untop ⋯))

Tactic:
]

Goal state after:
case inr
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
⊢ (embDomain f x).orderTop = ↑(f (x.orderTop.untop ⋯))
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inr.hx
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
z : Γ
hz : z ∈ x.support
hy : f z ∈ (embDomain f x).support
⊢ x.orderTop ≤ ↑z

Tactic:
]

Goal state after:
case inr.hx
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
z : Γ
hz : z ∈ x.support
hy : f z ∈ (embDomain f x).support
⊢ x.orderTop ≤ ↑z
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
⊢ (¬∀ (j : Γ), ↑j < i → x.coeff j = 0) ↔ ∃ j, ↑j < i ∧ x.coeff j ≠ 0

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
⊢ (¬∀ (j : Γ), ↑j < i → x.coeff j = 0) ↔ ∃ j, ↑j < i ∧ x.coeff j ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : LinearOrder Γ
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
H : ∀ j < i, x.coeff j = 0
h : x.order < i
this : x = 0
⊢ x = 0

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : LinearOrder Γ
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
H : ∀ j < i, x.coeff j = 0
h : x.order < i
this : x = 0
⊢ x = 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : LinearOrder Γ
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
h : x ≠ 0
⊢ (¬∀ j < i, x.coeff j = 0) ↔ ∃ j < i, x.coeff j ≠ 0

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : LinearOrder Γ
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
h : x ≠ 0
⊢ (¬∀ j < i, x.coeff j = 0) ↔ ∃ j < i, x.coeff j ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
⊢ ∀ j < n, (ofSuppBddBelow f ⋯).coeff j = 0

pp: Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
⊢ ofSuppBddBelow f ⋯ ≠ 0

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
⊢ ∀ j < n, (ofSuppBddBelow f ⋯).coeff j = 0

Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
⊢ ofSuppBddBelow f ⋯ ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ (AddOpposite.unop x).support = (AddOpposite.unop x).support

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ (AddOpposite.unop x).orderTop = (AddOpposite.unop x).orderTop

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ
inst✝ : DecidableLT Γ
c : Γ
x : R⟦Γ⟧
⊢ {y | y ∈ x.support ∧ y < c} ⊆ x.support

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ
inst✝ : DecidableLT Γ
c : Γ
x : R⟦Γ⟧
⊢ {y | y ∈ x.support ∧ y < c} ⊆ x.support
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ (AddOpposite.unop x).leadingCoeff = (AddOpposite.unop x).leadingCoeff

Tactic:
]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : x ≠ 0
hy : y ≠ 0
hxy : x + y ≠ 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯

Tactic:
]

Goal state after:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : x ≠ 0
hy : y ≠ 0
hxy : x + y ≠ 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯
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⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ min (⋯.min ⋯) (⋯.min ⋯) ≤ ⋯.min ⋯

Tactic:
]

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

Goal state before:
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 (⋯.min ⋯) (⋯.min ⋯) ≤ ⋯.min ⋯

Tactic:
]

Goal state after:
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 (⋯.min ⋯) (⋯.min ⋯) ≤ ⋯.min ⋯
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
⊢ x.coeff g ≠ 0

Tactic:
]

Goal state after:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
⊢ x.coeff g ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
hcxyne : (x + y).coeff g ≠ 0
⊢ (x + y).orderTop ≤ ↑(⋯.min ⋯)

Tactic:
]

Goal state after:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
hcxyne : (x + y).coeff g ≠ 0
⊢ (x + y).orderTop ≤ ↑(⋯.min ⋯)
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.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.orderTop
h : x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff
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.orderTop
h : x + y = 0
⊢ leadingCoeff 0 = leadingCoeff 0

Tactic:
]

Goal state after:
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.coeff (x.orderTop.untop ⋯) = x.coeff (x.orderTop.untop ⋯)

Tactic:
]

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

Goal state before:
pp: 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
h : x.order = y.order
hyne : 0 ≠ 0
⊢ False

Tactic:
]

Goal state after:
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
h : x.order = y.order
hyne : 0 ≠ 0
⊢ False
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:
· simpa using coeff_order_eq_zero.not.2 <| ne_zero_of_eq_add_single hxy hy

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: 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
⊢ x.coeff g = x.coeff g

Tactic:
]

Goal state after:
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
this : x.coeff g = y.coeff g
⊢ 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
this : x.coeff g = y.coeff g
⊢ g ∈ x.support
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_7
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s✝ : Finset α
x : α → R⟦Γ⟧
g : Γ
i : α
s : Finset α
his : i ∉ s
hsum : (∑ i ∈ s, x i).coeff g = ∑ i ∈ s, (x i).coeff g
⊢ (x i).coeff g + ∑ i ∈ s, (x i).coeff g = (x i).coeff g + ∑ x_1 ∈ s, (x x_1).coeff g

Tactic:
]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
⊢ min x.orderTop (-y).orderTop ≤ (x + -y).orderTop

Tactic:
]

Goal state after:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
⊢ min x.orderTop (-y).orderTop ≤ (x + -y).orderTop
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ (x + -y).orderTop = x.orderTop

Tactic:
]

Goal state after:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ (x + -y).orderTop = x.orderTop
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < (-y).orderTop
⊢ (x + -y).orderTop = x.orderTop

Tactic:
]

Goal state after:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < (-y).orderTop
⊢ (x + -y).orderTop = x.orderTop
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ (x + -y).leadingCoeff = x.leadingCoeff

Tactic:
]

Goal state after:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ (x + -y).leadingCoeff = x.leadingCoeff