mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : M₀
⊢ x ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y

Tactic:
obtain rfl | ⟨x, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
  obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y

Goal state after:
case inl.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ 0 ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

case inl.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : M₀ˣ
⊢ 0 ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y

case inr.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x : M₀ˣ
⊢ ↑x ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

case inr.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : M₀ˣ
⊢ ↑x ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : N₀
⊢ x ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y

Tactic:
obtain rfl | ⟨x, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
  obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y

Goal state after:
case inl.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ 0 ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

case inl.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : N₀ˣ
⊢ 0 ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y

case inr.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
x : N₀ˣ
⊢ ↑x ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

case inr.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : N₀ˣ
⊢ ↑x ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
f : Γ → R
h : (Function.support f).IsPWO
⊢ { coeff := f, isPWO_support' := h } = 0 ↔ f = 0

Tactic:
by
  simp_rw [HahnSeries.ext_iff, funext_iff, coeff_zero, Pi.zero_apply]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
⊢ ((single a) r).support ⊆ {a}

Tactic:
exact Pi.support_single_subset

Goal state after:
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 = x.leadingCoeff

Tactic:
orderTop_eq_top.mp ho.symm

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
⊢ leadingCoeff 0 = leadingCoeff 0
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 + y).leadingCoeff = x.leadingCoeff

Tactic:
· simp_rw [leadingCoeff_of_ne_zero h, leadingCoeff_of_ne_zero hx, ho, coeff_add]
    rw [coeff_eq_zero_of_lt_orderTop (x := y) (by simpa using hxy), add_zero]

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⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ (x - y).leadingCoeff = x.leadingCoeff

Tactic:
rw [sub_eq_add_neg]
  rw [← orderTop_neg (x := y)] at hxy
  exact leadingCoeff_add_eq_left hxy

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

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

Tactic:
simpa [heq] using archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex heq

Goal state after:
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:
rw [← abs_nsmul]

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.Multiplication

Goal state before:
pp: Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁷ : PartialOrder Γ'
inst✝⁶ : AddCommMonoid V
Γ : Type u_6
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : PartialOrder Γ
inst✝³ : AddAction Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
⊢ ((of R).symm ((single 0) r • x)).coeff a = r • ((of R).symm x).coeff a

Tactic:
nth_rw 1 [← zero_vadd Γ a]
  exact coeff_single_smul_vadd

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

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
⊢ f (∑ i ∈ s, l i) = f (l k)

Tactic:
by_cases hcard : s.card = 1

Goal state after:
case pos
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
hcard : s.card = 1
⊢ f (∑ i ∈ s, l i) = f (l k)

case neg
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommGroup α
f : α → R
fna : IsNonarchimedean f
f_neg : ∀ (a : α), f a = f (-a)
s : Finset β
l : β → α
k : β
hk : k ∈ s
hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)
hcard : ¬s.card = 1
⊢ f (∑ i ∈ s, l i) = f (l k)
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
⊢ f 0 = 0

Tactic:
by aesop

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
⊢ ∀ (x : α), 0 ≤ f x

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x : R
⊢ x * x ∈ P

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x : R
⊢ x ^ 2 ∈ P

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
S : Set R
hS : S = ↑P
a✝ b✝ : R
ha : a✝ ∈ S
hb : b✝ ∈ S
⊢ a✝ * b✝ ∈ S

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
S : Set R
hS : S = ↑P
⊢ 1 ∈ S

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
S : Set R
hS : S = ↑P
a✝ b✝ : R
ha : a✝ ∈ S
hb : b✝ ∈ S
⊢ a✝ + b✝ ∈ S

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
S : Set R
hS : S = ↑P
⊢ 0 ∈ S

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
⊢ ∀ {a b : R}, a ∈ ↑P ∩ -↑P → b ∈ ↑P ∩ -↑P → a + b ∈ ↑P ∩ -↑P

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
⊢ 0 ∈ ↑P ∩ -↑P

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
⊢ ∀ {x : R}, x ∈ ↑P ∩ -↑P → -x ∈ ↑P ∩ -↑P

Tactic:
by aesop

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
n : ℤ
x y : R
h : mk x = mk y
⊢ mk (x ^ n) = mk (y ^ n)

Tactic:
by
    obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg <;> simp [h]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R✝¹ : Type u_1
inst✝² : CommRing R✝¹
P✝¹ : RingPreordering R✝¹
R✝ : Type u_2
inst✝¹ : CommRing R✝
P✝ : Set R✝
add✝ : ?m.2
mul✝ : ?m.3
sq✝ : ?m.4
neg_one✝ : ?m.5
R : Type u_3
inst✝ : CommRing R
P : Set R
add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P
mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P
sq : ∀ (x : R), x * x ∈ P
neg_one : -1 ∉ P
x y : R
⊢ x ∈ P → y ∈ P → x * y ∈ P

Tactic:
by simpa using mul

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x✝¹ : P.IsOrdering
a b : R
x✝ : -(a * b) ∈ P
this : ¬(a ∈ P ∨ b ∈ P)
⊢ -a ∈ P

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x✝¹ : P.IsOrdering
a b : R
x✝ : -(a * b) ∈ P
this : ¬(a ∈ P ∨ b ∈ P)
⊢ -b ∈ P

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this✝⁴ : HasMemOrNegMem P
x y : R
x✝ : x * y ∈ P.support
this✝³ : ¬(x ∈ P.support ∨ y ∈ P.support)
this✝² : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this✝¹ : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this✝ : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
this : -(x * -y) ∈ P → x ∈ P ∨ -y ∈ P
⊢ x ∈ P ∨ -x ∈ P

Tactic:
by aesop

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
x : ↥(↑f).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ seed.stratum c
hx' : ↑x ∈ seed.baseEmbedding.domain
heq : ↑⟨↑x, hx'⟩ = ↑x
fx : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c) := DFinsupp.single c ⟨↑x, hx⟩
hfx : ↑x = fx.sum fun c ↦ ⇑(seed.stratum c).subtype
⊢ ofLex (↑seed.baseEmbedding ⟨↑x, hx'⟩) = ofLex (toLex ((single c) ((seed.coeff c) ⟨↑x, hx⟩)))

Tactic:
ofLex_toLex

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
x : ↥(↑f).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ seed.stratum c
hx' : ↑x ∈ seed.baseEmbedding.domain
heq : ↑⟨↑x, hx'⟩ = ↑x
fx : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c) := DFinsupp.single c ⟨↑x, hx⟩
hfx : ↑x = fx.sum fun c ↦ ⇑(seed.stratum c).subtype
⊢ ofLex (↑seed.baseEmbedding ⟨↑x, hx'⟩) = (single c) ((seed.coeff c) ⟨↑x, hx⟩)
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✝² : CommSemiring R
A : Type u_6
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
x : A⟦Γ⟧
x✝ : Γ
⊢ ((C.comp (algebraMap R A)) r * x).coeff x✝ = (x * (C.comp (algebraMap R A)) r).coeff x✝

Tactic:
simp only [coeff_smul, single_zero_mul_eq_smul, RingHom.coe_comp, C_apply,
      Function.comp_apply, algebraMap_smul, coeff_mul_single_zero]

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✝² : CommSemiring R
A : Type u_6
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
x : A⟦Γ⟧
x✝ : Γ
⊢ r • x.coeff x✝ = x.coeff x✝ * (algebraMap R A) r
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
y : ↥(↑f).domain
h : f.eval x = ↑↑f y
z : ↥(↑f).domain
this : x - ↑y = x - ↑z + (↑z - ↑y)
hyz : ¬↑z - ↑y = 0
c : FiniteArchimedeanClass M
hc : ↑c < ArchimedeanClass.mk (↑z - x)
⊢ (ofLex (toLex { coeff := f.evalCoeff x, isPWO_support' := ⋯ })).coeff c = (ofLex (↑↑f z)).coeff c

Tactic:
ofLex_toLex

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
y : ↥(↑f).domain
h : f.eval x = ↑↑f y
z : ↥(↑f).domain
this : x - ↑y = x - ↑z + (↑z - ↑y)
hyz : ¬↑z - ↑y = 0
c : FiniteArchimedeanClass M
hc : ↑c < ArchimedeanClass.mk (↑z - x)
⊢ f.evalCoeff x c = (ofLex (↑↑f z)).coeff c
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
h_2 : ¬x⁻¹ + 1 = 0
⊢ x ∈ B

Tactic:
rw [← valuation_le_one_iff, ← not_lt, Valuation.one_lt_val_iff _ h_1,
        ← add_sub_cancel_right x⁻¹, ← Units.val_mk0 h_2, ← mem_principalUnitGroup_iff] at hx ⊢

Goal state after:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx✝¹ : ¬A.valuation x⁻¹ < 1
h_1 : ¬x = 0
h_2 : ¬x⁻¹ + 1 = 0
hx✝ : ¬A.valuation (x⁻¹ + 1 - 1) < 1
hx : Units.mk0 (x⁻¹ + 1) h_2 ∉ A.principalUnitGroup
⊢ Units.mk0 (x⁻¹ + 1) h_2 ∉ B.principalUnitGroup
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case a
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
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
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this : ↑z ≠ x
hzyne : ↑z - ↑y ≠ 0
hzyclass : FiniteArchimedeanClass.mk (↑y - x) hxy0 = FiniteArchimedeanClass.mk (↑z - ↑y) hzyne
i : FiniteArchimedeanClass M
hj : ∀ j < i, (ofLex (↑↑f z)).coeff j = (ofLex (↑↑f y)).coeff j
hi : (ofLex (↑↑f z)).coeff i < (ofLex (↑↑f y)).coeff i
hlt : FiniteArchimedeanClass.mk (↑y - x) hxy0 < i
⊢ False

Tactic:
obtain hj := sub_eq_zero_of_eq (hj (mk _ hxy0) hlt)

Goal state after:
case a
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
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
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this : ↑z ≠ x
hzyne : ↑z - ↑y ≠ 0
hzyclass : FiniteArchimedeanClass.mk (↑y - x) hxy0 = FiniteArchimedeanClass.mk (↑z - ↑y) hzyne
i : FiniteArchimedeanClass M
hj✝ : ∀ j < i, (ofLex (↑↑f z)).coeff j = (ofLex (↑↑f y)).coeff j
hi : (ofLex (↑↑f z)).coeff i < (ofLex (↑↑f y)).coeff i
hlt : FiniteArchimedeanClass.mk (↑y - x) hxy0 < i
hj :
  (ofLex (↑↑f z)).coeff (FiniteArchimedeanClass.mk (↑y - x) hxy0) -
      (ofLex (↑↑f y)).coeff (FiniteArchimedeanClass.mk (↑y - x) hxy0) =
    0
⊢ False
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
⊢ ↑x ∈ A.principalUnitGroup ↔ A.unitGroupMulEquiv x ∈ (Units.map ↑(IsLocalRing.residue ↥A)).ker

Tactic:
rw [MonoidHom.mem_ker, Units.ext_iff]

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
⊢ ↑x ∈ A.principalUnitGroup ↔ ↑((Units.map ↑(IsLocalRing.residue ↥A)) (A.unitGroupMulEquiv x)) = ↑1
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 : ℝ →+*o K
hx : 0 ≤ mk x
⊢ (FiniteResidueField.ofArchimedean f) (stdPart x) = FiniteResidueField.mk (FiniteElement.mk x hx)

Tactic:
by
  rw [stdPart, dif_pos hx, ← OrderRingHom.comp_apply, ← OrderRingHom.comp_assoc,
    OrderRingHom.comp_apply, OrderRingHom.apply_eq_self]

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

Goal state before:
pp: case neg.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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
d : FiniteArchimedeanClass M
hdc : c ≤ d
⊢ (ofLex (toLex { coeff := f.evalCoeff x, isPWO_support' := ⋯ })).coeff d = 0

Tactic:
ofLex_toLex

Goal state after:
case neg.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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
d : FiniteArchimedeanClass M
hdc : c ≤ d
⊢ { coeff := f.evalCoeff x, isPWO_support' := ⋯ }.coeff d = 0
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case monomial
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
n✝ : ℕ
a✝ : A
⊢ x ^ n✝ • d' ((algebraMap A B) a✝) + (algebraMap A B) a✝ • n✝ • x ^ (n✝ - 1) • d' x =
    x ^ n✝ • d' ((algebraMap A B) a✝) + ((algebraMap A B) a✝ * ↑n✝ * x ^ (n✝ - 1)) • d' x

Tactic:
← smul_smul,

Goal state after:
case monomial
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
n✝ : ℕ
a✝ : A
⊢ x ^ n✝ • d' ((algebraMap A B) a✝) + (algebraMap A B) a✝ • n✝ • x ^ (n✝ - 1) • d' x =
    x ^ n✝ • d' ((algebraMap A B) a✝) + ((algebraMap A B) a✝ * ↑n✝) • x ^ (n✝ - 1) • d' x
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case monomial
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
n✝ : ℕ
a✝ : A
⊢ x ^ n✝ • d' ((algebraMap A B) a✝) + (algebraMap A B) a✝ • n✝ • x ^ (n✝ - 1) • d' x =
    x ^ n✝ • d' ((algebraMap A B) a✝) + ((algebraMap A B) a✝ * ↑n✝) • x ^ (n✝ - 1) • d' x

Tactic:
← smul_smul,

Goal state after:
case monomial
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
n✝ : ℕ
a✝ : A
⊢ x ^ n✝ • d' ((algebraMap A B) a✝) + (algebraMap A B) a✝ • n✝ • x ^ (n✝ - 1) • d' x =
    x ^ n✝ • d' ((algebraMap A B) a✝) + (algebraMap A B) a✝ • ↑n✝ • x ^ (n✝ - 1) • d' x