mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
⊢ (A.ofPrime P).valuation ↑x = 1 ↔ (A.ofPrime P).valuation ↑((algebraMap ↥A ↥(A.ofPrime P)) x) = 1

Tactic:
]

Goal state after:
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
⊢ (A.ofPrime P).valuation ↑x = 1 ↔ (A.ofPrime P).valuation ↑((algebraMap ↥A ↥(A.ofPrime P)) x) = 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ 1 ≤ S.valuation ((algebraMap (↥R) K) r)

pp: case a.ha
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ 0 < S.valuation ((algebraMap (↥R) K) r)

pp: case a.hb
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ 0 < 1

Tactic:
]

Goal state after:
case a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ 1 ≤ S.valuation ((algebraMap (↥R) K) r)

case a.ha
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ 0 < S.valuation ((algebraMap (↥R) K) r)

case a.hb
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ 0 < 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
R S : ValuationSubring K
h✝ : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
h : x = 0
⊢ 0 ∈ R

Tactic:
]

Goal state after:
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h✝ : R ≤ S
x : K
hx : x ∈ S
hr : x ∉ R
h : x = 0
⊢ 0 ∈ R
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : 1 ≤ S.valuation ↑((A.inclusion R hR) x)
⊢ False

Tactic:
]

Goal state after:
K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : 1 ≤ S.valuation ↑((A.inclusion R hR) x)
⊢ False
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
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ArchimedeanClass.mk (↑y - x) = ↑c
h : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
⊢ { coeff := f.evalCoeff x, isPWO_support' := ⋯ } = (truncLTLinearMap K c) (ofLex (↑↑f y))

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
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
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ArchimedeanClass.mk (↑y - x) = ↑c
h : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
⊢ { coeff := f.evalCoeff x, isPWO_support' := ⋯ } = (truncLTLinearMap K c) (ofLex (↑↑f y))
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
P : PrimeSpectrum ↥A
⊢ (fun S ↦ { asIdeal := A.idealOfLE ↑S ⋯, isPrime := ⋯ }) ((fun P ↦ ⟨A.ofPrime P.asIdeal, ⋯⟩) P) = P

Tactic:
by ext1; simp

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
S : { S // A ≤ S }
⊢ (fun P ↦ ⟨A.ofPrime P.asIdeal, ⋯⟩) ((fun S ↦ { asIdeal := A.idealOfLE ↑S ⋯, isPrime := ⋯ }) S) = S

Tactic:
by ext1; simp

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : α →ₙ+ β
hf : Monotone ⇑f
a b : α
⊢ f a ≤ f (a - b + b)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : α →ₙ+ β
hf : Monotone ⇑f
a b : α
⊢ f a ≤ f (a - b + b)
Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹² : PartialOrder α
inst✝¹¹ : AddCommSemigroup α
inst✝¹⁰ : ExistsAddOfLE α
inst✝⁹ : AddLeftMono α
inst✝⁸ : Sub α
inst✝⁷ : OrderedSub α
inst✝⁶ : PartialOrder β
inst✝⁵ : AddCommSemigroup β
inst✝⁴ : Sub β
inst✝³ : OrderedSub β
inst✝² : AddLeftReflectLE β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f (a - b) = f (a - b)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case refine_3
K : Type u
inst✝ : Field K
A : ValuationSubring K
a✝ b✝ : (PrimeSpectrum ↥A)ᵒᵈ
a b : PrimeSpectrum ↥A
h : ⟨A.ofPrime a.asIdeal, ⋯⟩ ≤ ⟨A.ofPrime b.asIdeal, ⋯⟩
this : b.asIdeal ≤ a.asIdeal
⊢ b ≤ a

Tactic:
]

Goal state after:
case refine_3
K : Type u
inst✝ : Field K
A : ValuationSubring K
a✝ b✝ : (PrimeSpectrum ↥A)ᵒᵈ
a b : PrimeSpectrum ↥A
h : ⟨A.ofPrime a.asIdeal, ⋯⟩ ≤ ⟨A.ofPrime b.asIdeal, ⋯⟩
this : b.asIdeal ≤ a.asIdeal
⊢ b ≤ a
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case 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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ArchimedeanClass.mk (↑y - x) = ↑c
h : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
d : FiniteArchimedeanClass M
hd : d < c
⊢ f.evalCoeff x d = (ofLex (↑↑f y)).coeff d

Tactic:
]

Goal state after:
case 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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ArchimedeanClass.mk (↑y - x) = ↑c
h : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
d : FiniteArchimedeanClass M
hd : d < c
⊢ f.evalCoeff x d = (ofLex (↑↑f y)).coeff d
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case 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
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ArchimedeanClass.mk (↑y - x) = ↑c
h : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
d : FiniteArchimedeanClass M
hd : c ≤ d
⊢ f.evalCoeff x d = 0

Tactic:
]

Goal state after:
case 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
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ArchimedeanClass.mk (↑y - x) = ↑c
h : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
d : FiniteArchimedeanClass M
hd : c ≤ d
⊢ f.evalCoeff x d = 0
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝² : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
inst✝ : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.valuationSubring = v₂.valuationSubring
x : K
⊢ x ∈ v₂.valuationSubring ↔ x ∈ v₂.valuationSubring

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝¹ : Field K
Γ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ ∀ {x : K}, v x ≤ 1 ↔ v.valuationSubring.valuation x ≤ 1

Tactic:
]

Goal state after:
K : Type u
inst✝¹ : Field K
Γ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ ∀ {x : K}, v x ≤ 1 ↔ v.valuationSubring.valuation x ≤ 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝¹ : Field K
Γ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
x : K
⊢ v x ≤ 1 ↔ v x ≤ 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : K
⊢ x✝ ∈ A.valuation.valuationSubring ↔ A.valuation x✝ ≤ 1

Tactic:
]

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x✝ : K
⊢ x✝ ∈ A.valuation.valuationSubring ↔ A.valuation x✝ ≤ 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
⊢ x ∈ B

Tactic:
]

Goal state after:
case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
⊢ x ∈ B
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
y : ↥(↑f).domain
c : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (↑y - x) ⋯
hc : ArchimedeanClass.mk (↑y - x) = ↑c
this : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
x' : ↥(↑f).domain
h : f.eval x = (↑f).toFun x'
hx' : (↑f).toFun x' = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
⊢ x ∈ (↑f).domain

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
y : ↥(↑f).domain
c : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (↑y - x) ⋯
hc : ArchimedeanClass.mk (↑y - x) = ↑c
this : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
x' : ↥(↑f).domain
h : f.eval x = (↑f).toFun x'
hx' : (↑f).toFun x' = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
⊢ x ∈ (↑f).domain
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x : K
⊢ x ∈ A.nonunits ↔ x ∈ A.nonunits

pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x : K
⊢ x = 0 → x ∈ A.nonunits

Tactic:
]

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : K
⊢ x = 0 → x ∈ A.nonunits
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x : K
⊢ x = 0 ∨ x ∉ A ↔ x = 0 ∨ x ∉ A

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
y : ↥(↑f).domain
h : x < ↑y
⊢ ∃ i,
    (∀ j < i, (ofLex (f.eval x)).coeff j = (ofLex (↑↑f y)).coeff j) ∧
      (ofLex (f.eval x)).coeff i < (ofLex (↑↑f y)).coeff i

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
y : ↥(↑f).domain
h : x < ↑y
⊢ ∃ i,
    (∀ j < i, (ofLex (f.eval x)).coeff j = (ofLex (↑↑f y)).coeff j) ∧
      (ofLex (f.eval x)).coeff i < (ofLex (↑↑f y)).coeff i
Module: Mathlib.RingTheory.Valuation.ValuationSubring

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

Tactic:
]

Goal state after:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : ¬A.valuation x⁻¹ < 1
h_1 : ¬x = 0
⊢ ¬B.valuation x⁻¹ < 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : K
⊢ (∃ a_1, ∃ (b : a_1 ∈ A), ⟨a_1, b⟩ ∈ IsLocalRing.maximalIdeal ↥A ∧ ↑⟨a_1, b⟩ = a) ↔
    ∃ (ha : a ∈ A), ⟨a, ha⟩ ∈ IsLocalRing.maximalIdeal ↥A

Tactic:
]

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : K
⊢ (∃ a_1, ∃ (b : a_1 ∈ A), ⟨a_1, b⟩ ∈ IsLocalRing.maximalIdeal ↥A ∧ ↑⟨a_1, b⟩ = a) ↔
    ∃ (ha : a ∈ A), ⟨a, ha⟩ ∈ IsLocalRing.maximalIdeal ↥A
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : Kˣ
ha : A.valuation (↑a - 1) < 1
hb : A.valuation (↑b - 1) < 1
⊢ A.valuation (↑(a * b) - 1) < 1

Tactic:
]

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : Kˣ
ha : A.valuation (↑a - 1) < 1
hb : A.valuation (↑b - 1) < 1
⊢ A.valuation (↑(a * b) - 1) < 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : Kˣ
ha : A.valuation (↑a - 1) < 1
hb : A.valuation (↑b - 1) < 1
⊢ A.valuation (↑(a * b) - ?b + (?b - 1)) ≤ max (A.valuation (↑a * ↑b - ↑a)) (A.valuation (↑a - 1))

pp: case b
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : Kˣ
ha : A.valuation (↑a - 1) < 1
hb : A.valuation (↑b - 1) < 1
⊢ K

Tactic:
]

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : Kˣ
ha : A.valuation (↑a - 1) < 1
hb : A.valuation (↑b - 1) < 1
⊢ A.valuation (↑(a * b) - ?b + (?b - 1)) ≤ max (A.valuation (↑a * ↑b - ↑a)) (A.valuation (↑a - 1))

case b
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : Kˣ
ha : A.valuation (↑a - 1) < 1
hb : A.valuation (↑b - 1) < 1
⊢ K
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
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) ⋯)
⊢ (ofLex (↑↑f z)).coeff (FiniteArchimedeanClass.mk (↑y - x) ⋯) <
    (ofLex (↑↑f y)).coeff (FiniteArchimedeanClass.mk (↑y - x) hxy0)

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
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) ⋯)
⊢ (ofLex (↑↑f z)).coeff (FiniteArchimedeanClass.mk (↑y - x) ⋯) <
    (ofLex (↑↑f y)).coeff (FiniteArchimedeanClass.mk (↑y - x) hxy0)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : Kˣ
ha : A.valuation (↑a - 1) < 1
⊢ A.valuation (↑a - 1) < 1

Tactic:
]

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : Kˣ
ha : A.valuation (↑a - 1) < 1
⊢ A.valuation (↑a - 1) < 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case pos
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
⊢ x ∈ B

Tactic:
]

Goal state after:
case pos
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
⊢ x ∈ B
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
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
hzy : z < y
hzyne : ↑z - ↑y ≠ 0
this : ↑y - ↑z = ↑y - x + (x - ↑z)
⊢ ArchimedeanClass.mk (↑y - x) = ArchimedeanClass.mk (↑y - x + (x - ↑z))

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
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
hzy : z < y
hzyne : ↑z - ↑y ≠ 0
this : ↑y - ↑z = ↑y - x + (x - ↑z)
⊢ ArchimedeanClass.mk (↑y - x) = ArchimedeanClass.mk (↑y - x + (x - ↑z))
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
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
hzy : z < y
hzyne : ↑z - ↑y ≠ 0
this : ↑y - ↑z = ↑y - x + (x - ↑z)
⊢ ArchimedeanClass.mk (↑y - x) < ArchimedeanClass.mk (↑z - 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
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
hzy : z < y
hzyne : ↑z - ↑y ≠ 0
this : ↑y - ↑z = ↑y - x + (x - ↑z)
⊢ ArchimedeanClass.mk (↑y - x) < ArchimedeanClass.mk (↑z - x)
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✝¹ : ¬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

Tactic:
]

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 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
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
hzy :
  ∃ i, (∀ j < i, (ofLex (↑↑f z)).coeff j = (ofLex (↑↑f y)).coeff j) ∧ (ofLex (↑↑f z)).coeff i < (ofLex (↑↑f y)).coeff i
hzyne : ↑z - ↑y ≠ 0
hzyclass : FiniteArchimedeanClass.mk (↑y - x) hxy0 = FiniteArchimedeanClass.mk (↑z - ↑y) hzyne
⊢ (ofLex (↑↑f z)).coeff (FiniteArchimedeanClass.mk (↑y - x) ⋯) <
    (ofLex (↑↑f y)).coeff (FiniteArchimedeanClass.mk (↑y - x) hxy0)

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
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
hzy :
  ∃ i, (∀ j < i, (ofLex (↑↑f z)).coeff j = (ofLex (↑↑f y)).coeff j) ∧ (ofLex (↑↑f z)).coeff i < (ofLex (↑↑f y)).coeff i
hzyne : ↑z - ↑y ≠ 0
hzyclass : FiniteArchimedeanClass.mk (↑y - x) hxy0 = FiniteArchimedeanClass.mk (↑z - ↑y) hzyne
⊢ (ofLex (↑↑f z)).coeff (FiniteArchimedeanClass.mk (↑y - x) ⋯) <
    (ofLex (↑↑f y)).coeff (FiniteArchimedeanClass.mk (↑y - x) hxy0)