mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
⊢ 0 < ↑(f.extendFun hx) ⟨a + b, ⋯⟩

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
⊢ 0 < ↑(f.extendFun hx) ⟨a + b, ⋯⟩
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : stabilizer G t ≤ stabilizer G s
hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G s
⊢ stabilizer G t = stabilizer G t

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ b <• a ∈ b •> s

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ b <• a ∈ b •> s
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ a ∈ s

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
a : G
s : Set G
ha : a ∈ s
b : G
hb : b ∈ ↑(stabilizer G s)
⊢ a ∈ s
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case div
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
n : ℤ
d : ℕ
hd : d ≠ 0
a✝ : n.natAbs.Coprime d
⊢ mk (FiniteElement.mk (↑(↑n / ↑d) * ↑d) ⋯) = ↑(↑n / ↑d) * mk (FiniteElement.mk ↑d ⋯)

Tactic:
]

Goal state after:
case div
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
n : ℤ
d : ℕ
hd : d ≠ 0
a✝ : n.natAbs.Coprime d
⊢ mk (FiniteElement.mk (↑(↑n / ↑d) * ↑d) ⋯) = ↑(↑n / ↑d) * mk (FiniteElement.mk ↑d ⋯)
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
⊢ 0 < ↑↑f ⟨a, ha⟩ + (RingHom.id K) c • f.eval 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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
⊢ 0 < ↑↑f ⟨a, ha⟩ + (RingHom.id K) c • f.eval x
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ s = a • s ↔ s = a • s

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ a • s = s ↔ a • s = s

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ s ⊆ a⁻¹ • s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s

Tactic:
]

Goal state after:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ s ⊆ a⁻¹ • s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : R →+*o K
⊢ ∀ (a : R), (ofArchimedean f) a = 0 → a = 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : R →+*o K
⊢ ∀ (a : R), (ofArchimedean f) a = 0 → a = 0
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Finset α
⊢ s ⊆ a • s ↔ s ⊆ a • s

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : R →+*o K
r : R
hr : r ≠ 0
⊢ ArchimedeanClass.mk ↑(FiniteElement.mk (f r) ⋯) = 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : R →+*o K
r : R
hr : r ≠ 0
⊢ ArchimedeanClass.mk ↑(FiniteElement.mk (f r) ⋯) = 0
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this✝ : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
this : -(c • f.eval x) < ↑↑f ⟨a, ha⟩
⊢ 0 < ↑↑f ⟨a, ha⟩ + (RingHom.id K) c • f.eval 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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this✝ : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
this : -(c • f.eval x) < ↑↑f ⟨a, ha⟩
⊢ 0 < ↑↑f ⟨a, ha⟩ + (RingHom.id K) c • f.eval x
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Finset α
⊢ a • s ⊆ s ↔ a • s ⊆ s

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : FiniteResidueField K →+*o ℝ
h : 0 ≤ mk x
⊢ Classical.ofNonempty (FiniteResidueField.mk (FiniteElement.mk x h)) = f (FiniteResidueField.mk (FiniteElement.mk x h))

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : FiniteResidueField K →+*o ℝ
h : 0 ≤ mk x
⊢ Classical.ofNonempty (FiniteResidueField.mk (FiniteElement.mk x h)) = f (FiniteResidueField.mk (FiniteElement.mk x h))
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
s : Set G
⊢ s = s

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: case H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)
⊢ QuotientGroup.mk '' (a • s) = QuotientGroup.mk '' s ↔ a • s = s

Tactic:
]

Goal state after:
case H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)
⊢ QuotientGroup.mk '' (a • s) = QuotientGroup.mk '' s ↔ a • s = s
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)
h : a • s = s
⊢ QuotientGroup.mk '' s = QuotientGroup.mk '' s

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: case H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)
h : a • s = s
⊢ a • s = s

Tactic:
]

Goal state after:
case H
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)
h : a • s = s
⊢ a • s = s
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h : mk x = 0
⊢ mk ↑(FiniteElement.mk x ⋯) = 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h : mk x = 0
⊢ mk ↑(FiniteElement.mk x ⋯) = 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h✝ : mk x ≠ 0
h : 0 < mk x
⊢ 0 = 0

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
⊢ -(c • x) < a

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
⊢ -(c • x) < a
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : 0 ≤ mk x
y : K
hy : 0 ≤ mk y
h : x ≤ y
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) ≤
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y hy)

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : 0 ≤ mk x
y : K
hy : 0 ≤ mk y
h : x ≤ y
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) ≤
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y hy)
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : 0 ≤ mk x
y : K
hy : 0 ≤ mk y
h : x ≤ y
⊢ x ≤ y

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : 0 ≤ mk x
y : K
hy : 0 ≤ mk y
h : x ≤ y
⊢ x ≤ y
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk 0 ?hc) = 0

pp: case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ 0 ≤ mk 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk 0 ?hc) = 0

case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ 0 ≤ mk 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk 1 ?hc) = 1

pp: case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ 0 ≤ mk 1

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk 1 ?hc) = 1

case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ 0 ≤ mk 1
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case pos
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h✝ : 0 ≤ mk x
⊢ -(Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x ?pos✝) =
    -(Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x h✝)

pp: case pos
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h✝ : 0 ≤ mk x
⊢ 0 ≤ mk x

Tactic:
]

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

Goal state before:
pp: case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
hx' : 0 ≤ mk x⁻¹
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x⁻¹ hx') =
    ((Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x ⋯))⁻¹

Tactic:
]

Goal state after:
case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
hx' : 0 ≤ mk x⁻¹
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x⁻¹ hx') =
    ((Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x ⋯))⁻¹
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
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc✝ : c • x = b
hac : -0 • x < a
hc : c = 0
⊢ f.eval (-0 • x) < ↑↑f ⟨a, ha⟩

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
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc✝ : c • x = b
hac : -0 • x < a
hc : c = 0
⊢ f.eval (-0 • x) < ↑↑f ⟨a, ha⟩
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
hx' : 0 ≤ mk x⁻¹
this : FiniteElement.mk x⁻¹ hx' * FiniteElement.mk x ⋯ = 1
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ 0 = 0

pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ mk x⁻¹ ≠ 0

Tactic:
]

Goal state after:
case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ mk x⁻¹ ≠ 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ mk x ≠ 0

Tactic:
]

Goal state after:
case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ mk x ≠ 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x + y) ?hc) =
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) +
      (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y hy)

pp: case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ 0 ≤ mk (x + y)

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x + y) ?hc) =
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) +
      (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y hy)

case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ 0 ≤ mk (x + y)
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
hy : 0 ≤ mk y
⊢ stdPart y = stdPart y

Tactic:
]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
hy : mk y < 0
⊢ 0 = 0

pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
hy : mk y < 0
⊢ mk (x + y) ≠ 0

Tactic:
]

Goal state after:
case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
hy : mk y < 0
⊢ mk (x + y) ≠ 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
hy : mk y < 0
⊢ mk y ≠ 0

Tactic:
]

Goal state after:
case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
hy : mk y < 0
⊢ mk y ≠ 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hy : 0 < mk y
⊢ stdPart x = stdPart x

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ stdPart x + -stdPart y = stdPart x + -stdPart y

pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ 0 ≤ mk (-y)

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ 0 ≤ mk (-y)
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ 0 ≤ mk y

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ 0 ≤ mk y
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
⊢ -stdPart y = -stdPart y

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x * y) ?hc) =
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) *
      (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y hy)

pp: case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ 0 ≤ mk (x * y)

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk (x * y) ?hc) =
    (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x hx) *
      (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk y hy)

case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ 0 ≤ mk (x * y)