mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x : R
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : x.leadingCoeff ≠ 0
hy : y.leadingCoeff ≠ 0
hxy : (x * y).coeff (x.order + y.order) ≠ 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : x.leadingCoeff ≠ 0
hy : y.leadingCoeff ≠ 0
hxy : (x * y).coeff (x.order + y.order) ≠ 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
n : ℕ
x : R
⊢ -(↑n • mk x + mk x) = -(↑n • mk x + mk x)

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝¹² : DivisionRing K
inst✝¹¹ : LinearOrder K
inst✝¹⁰ : IsOrderedRing K
inst✝⁹ : Archimedean K
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : Module K M
inst✝⁴ : IsOrderedModule K M
R : Type u_3
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : Module K R
seed : Seed K M R
inst✝ : IsOrderedAddMonoid R
x y : ↥seed.baseEmbedding.domain
h : x < y
⊢ 0 < ↑seed.baseEmbedding (y - x)

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹² : DivisionRing K
inst✝¹¹ : LinearOrder K
inst✝¹⁰ : IsOrderedRing K
inst✝⁹ : Archimedean K
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : Module K M
inst✝⁴ : IsOrderedModule K M
R : Type u_3
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : Module K R
seed : Seed K M R
inst✝ : IsOrderedAddMonoid R
x y : ↥seed.baseEmbedding.domain
h : x < y
⊢ 0 < ↑seed.baseEmbedding (y - x)
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
⊢ mk x + -mk y = mk x + -mk y

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case inr
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
q : ℚ
hn : q ≠ 0
⊢ 0 ≤ 0

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h✝ : Nontrivial R
⊢ ¬x = 0

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h✝ : Nontrivial R
⊢ ¬x = 0
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h✝ : Nontrivial R
hrx : ((single g) r).leadingCoeff * x.leadingCoeff ≠ 0
⊢ g + x.order = g + x.order

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∑ ij ∈ antidiagonal ⋯ ⋯ b, (x * y).coeff ij.1 * z.coeff ij.2 =
    ∑ ij ∈ antidiagonal ⋯ ⋯ b, x.coeff ij.1 * (y * z).coeff ij.2

Tactic:
]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∑ ij ∈ antidiagonal ⋯ ⋯ b, (x * y).coeff ij.1 * z.coeff ij.2 =
    ∑ ij ∈ antidiagonal ⋯ ⋯ b, x.coeff ij.1 * (y * z).coeff ij.2
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ n • x.orderTop + 1 • x.orderTop ≤ (x ^ n * x ^ 1).orderTop

Tactic:
]

Goal state after:
case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ n • x.orderTop + 1 • x.orderTop ≤ (x ^ n * x ^ 1).orderTop
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ (x ^ n).orderTop + x.orderTop = (x ^ n).orderTop + x.orderTop

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ (x ^ n * x).orderTop ≤ (x ^ n * x).orderTop

Tactic:
]

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

Goal state before:
pp: case mp.left
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
hx : 0 < (x - 1).orderTop
⊢ (1 + (x - 1)).orderTop = orderTop 1

Tactic:
]

Goal state after:
case mp.left
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
hx : 0 < (x - 1).orderTop
⊢ (1 + (x - 1)).orderTop = orderTop 1
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case mp.right
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
hx : 0 < (x - 1).orderTop
⊢ (1 + (x - 1)).leadingCoeff = leadingCoeff 1

Tactic:
]

Goal state after:
case mp.right
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
hx : 0 < (x - 1).orderTop
⊢ (1 + (x - 1)).leadingCoeff = leadingCoeff 1
Module: Mathlib.RingTheory.HahnSeries.Multiplication

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

Tactic:
]

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
⊢ ∃ f, (f.sum fun x xi ↦ ↑xi) = f'.sum fun d x ↦ ↑x

Tactic:
]

Goal state after:
case refine_1
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
⊢ ∃ f, (f.sum fun x xi ↦ ↑xi) = f'.sum fun d x ↦ ↑x
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧ˣ
hx : (↑x).orderTop = 0 ∧ (↑x).leadingCoeff = 1
hy : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
h✝ : Nontrivial R
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case inr.left
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧ˣ
hx : (↑x).orderTop = 0 ∧ (↑x).leadingCoeff = 1
hy : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
h✝ : Nontrivial R
h1 : (↑x).leadingCoeff * (↑y).leadingCoeff = 1
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
⊢ ofLex (↑seed.baseEmbedding ⟨f'.sum fun d x ↦ ↑x, ⋯⟩) = (truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))

Tactic:
]

Goal state after:
case refine_2
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
⊢ ofLex (↑seed.baseEmbedding ⟨f'.sum fun d x ↦ ↑x, ⋯⟩) = (truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case inr.right
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧ˣ
hx : (↑x).orderTop = 0 ∧ (↑x).leadingCoeff = 1
hy : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
h✝ : Nontrivial R
h1 : (↑x).leadingCoeff * (↑y).leadingCoeff = 1
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
d : FiniteArchimedeanClass M
⊢ (seed.coeff d) (f' d) = ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))).coeff d

Tactic:
]

Goal state after:
case refine_2
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
d : FiniteArchimedeanClass M
⊢ (seed.coeff d) (f' d) = ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))).coeff d
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case inr
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Nontrivial R
this : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
⊢ 0 < (y.inv - 1).orderTop

Tactic:
]

Goal state after:
case inr
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Nontrivial R
this : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
⊢ 0 < (y.inv - 1).orderTop
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Nontrivial R
this : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
⊢ y.inv.leadingCoeff ≠ 0

Tactic:
]

Goal state after:
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Nontrivial R
this : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
⊢ y.inv.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2.inl
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
d : FiniteArchimedeanClass M
hdc : d < c
⊢ (seed.coeff d) ((DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d) d) = (seed.coeff d) (f d)

Tactic:
]

Goal state after:
case refine_2.inl
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
d : FiniteArchimedeanClass M
hdc : d < c
⊢ (seed.coeff d) ((DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d) d) = (seed.coeff d) (f d)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∑ ij ∈ VAddAntidiagonal b ⋯, (x * y).coeff ij.1 • ((of R).symm z).coeff ij.2 =
    ∑ ij ∈ VAddAntidiagonal b ⋯, x.coeff ij.1 • ((of R).symm (y • z)).coeff ij.2

Tactic:
]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∑ ij ∈ VAddAntidiagonal b ⋯, (x * y).coeff ij.1 • ((of R).symm z).coeff ij.2 =
    ∑ ij ∈ VAddAntidiagonal b ⋯, x.coeff ij.1 • ((of R).symm (y • z)).coeff ij.2
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2.inr
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
d : FiniteArchimedeanClass M
hdc : c ≤ d
⊢ (seed.coeff d) ((DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d) d) = 0

Tactic:
]

Goal state after:
case refine_2.inr
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
d : FiniteArchimedeanClass M
hdc : c ≤ d
⊢ (seed.coeff d) ((DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d) d) = 0
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
r : R
x : R⟦Γ⟧
a : HahnModule Γ' R V
⊢ (single 0) r • x • a = (single 0) r • x • a

Tactic:
]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : CommSemiring R
inst✝ : Module R V
r : R
x : R⟦Γ⟧
y : HahnModule Γ' R V
⊢ x • r • y = x • r • y

Tactic:
]

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

Goal state before:
pp: Γ✝ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V✝ : Type u_5
inst✝¹⁴ : AddCommMonoid Γ✝
inst✝¹³ : PartialOrder Γ✝
inst✝¹² : IsOrderedCancelAddMonoid Γ✝
inst✝¹¹ : PartialOrder Γ'
inst✝¹⁰ : AddAction Γ✝ Γ'
inst✝⁹ : IsOrderedCancelVAdd Γ✝ Γ'
inst✝⁸ : AddCommMonoid V✝
Γ : Type u_6
V : Type u_7
inst✝⁷ : Ring R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup V
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Module R V
inst✝ : Module.IsTorsionFree R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hxy : x ≠ 0 ∧ y ≠ 0
⊢ ∃ x_1, ¬((of R).symm (x • y)).coeff x_1 = ((of R).symm 0).coeff x_1

Tactic:
]

Goal state after:
Γ✝ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V✝ : Type u_5
inst✝¹⁴ : AddCommMonoid Γ✝
inst✝¹³ : PartialOrder Γ✝
inst✝¹² : IsOrderedCancelAddMonoid Γ✝
inst✝¹¹ : PartialOrder Γ'
inst✝¹⁰ : AddAction Γ✝ Γ'
inst✝⁹ : IsOrderedCancelVAdd Γ✝ Γ'
inst✝⁸ : AddCommMonoid V✝
Γ : Type u_6
V : Type u_7
inst✝⁷ : Ring R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup V
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Module R V
inst✝ : Module.IsTorsionFree R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hxy : x ≠ 0 ∧ y ≠ 0
⊢ ∃ x_1, ¬((of R).symm (x • y)).coeff x_1 = ((of R).symm 0).coeff x_1
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
x a : R
h₁a : a ∈ P
h₂a : -a ∈ P
⊢ x * a ∈ P

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
x a : R
h₁a : a ∈ P
h₂a : -a ∈ P
⊢ x * a ∈ P
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
x a : R
h₁a : a ∈ P
h₂a : -a ∈ P
⊢ -(x * a) ∈ P

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
x a : R
h₁a : a ∈ P
h₂a : -a ∈ P
⊢ -(x * a) ∈ P
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y : α
⊢ (⟦x⟧ ≤ ⟦y⟧) = (x ≤ y ∨ x ≈ y)

Tactic:
]

Goal state after:
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y : α
⊢ (⟦x⟧ ≤ ⟦y⟧) = (x ≤ y ∨ x ≈ y)
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : IsUnit 2
⊢ ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : IsUnit 2
⊢ ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : IsUnit 2
x a : R
a✝¹ : a ∈ P
a✝ : -a ∈ P
half : R
h2 : 2 * half = 1
y : R := (1 + x) * half
z : R := (1 - x) * half
⊢ (y ^ 2 - z ^ 2) * a ∈ P ∧ -((y ^ 2 - z ^ 2) * a) ∈ P

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : IsUnit 2
x a : R
a✝¹ : a ∈ P
a✝ : -a ∈ P
half : R
h2 : 2 * half = 1
y : R := (1 + x) * half
z : R := (1 - x) * half
⊢ (y ^ 2 - z ^ 2) * a ∈ P ∧ -((y ^ 2 - z ^ 2) * a) ∈ P
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : x = a + b
⊢ ((single a) r).coeff a * s = ((single (a + b)) (r * s)).coeff (a + b)

Tactic:
]

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : x = a + b
⊢ ((single a) r).coeff a * s = ((single (a + b)) (r * s)).coeff (a + b)