case mp
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ IsEquiv v v' → ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1

case mpr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1) → IsEquiv v v'
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
constructor
case mp
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : IsEquiv v v'
x : K
⊢ ↑v x = 1 ↔ ↑v' x = 1
case mp
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ IsEquiv v v' → ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
intro h x
no goals
case mp
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : IsEquiv v v'
x : K
⊢ ↑v x = 1 ↔ ↑v' x = 1
simpa using @IsEquiv.val_eq _ _ _ _ _ _ v v' h x 1
case mpr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
⊢ IsEquiv v v'
case mpr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1) → IsEquiv v v'
intro h
case mpr.h
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
⊢ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
case mpr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
⊢ IsEquiv v v'
apply isEquiv_of_val_le_one
case mpr.h
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
⊢ ↑v x ≤ 1 ↔ ↑v' x ≤ 1
case mpr.h
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
⊢ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
intro x
case mpr.h.mp
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
⊢ ↑v x ≤ 1 → ↑v' x ≤ 1

case mpr.h.mpr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
⊢ ↑v' x ≤ 1 → ↑v x ≤ 1
case mpr.h
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
⊢ ↑v x ≤ 1 ↔ ↑v' x ≤ 1
constructor
case mpr.h.mp
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
⊢ ↑v' x ≤ 1
case mpr.h.mp
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
⊢ ↑v x ≤ 1 → ↑v' x ≤ 1
intro hx
case mpr.h.mp.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
⊢ ↑v' x ≤ 1

case mpr.h.mp.inr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x = 1
⊢ ↑v' x ≤ 1
case mpr.h.mp
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
⊢ ↑v' x ≤ 1
cases' lt_or_eq_of_le hx with hx' hx'
case mpr.h.mp.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
this : ↑v (1 + x) = 1
⊢ ↑v' x ≤ 1
case mpr.h.mp.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
⊢ ↑v' x ≤ 1
have : v (1 + x) = 1 := by
  rw [← v.map_one]
  apply map_add_eq_of_lt_left
  simpa
case mpr.h.mp.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
this : ↑v' (1 + x) = 1
⊢ ↑v' x ≤ 1
case mpr.h.mp.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
this : ↑v (1 + x) = 1
⊢ ↑v' x ≤ 1
rw [h] at this
case mpr.h.mp.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
this : ↑v' (1 + x) = 1
⊢ ↑v' (-1 + (1 + x)) ≤ 1
case mpr.h.mp.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
this : ↑v' (1 + x) = 1
⊢ ↑v' x ≤ 1
rw [show x = -1 + (1 + x) by simp]
case mpr.h.mp.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
this : ↑v' (1 + x) = 1
⊢ max (↑v' (-1)) (↑v' (1 + x)) ≤ 1
case mpr.h.mp.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
this : ↑v' (1 + x) = 1
⊢ ↑v' (-1 + (1 + x)) ≤ 1
refine' le_trans (v'.map_add _ _) _
no goals
case mpr.h.mp.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
this : ↑v' (1 + x) = 1
⊢ max (↑v' (-1)) (↑v' (1 + x)) ≤ 1
simp [this]
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
⊢ ↑v (1 + x) = ↑v 1
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
⊢ ↑v (1 + x) = 1
rw [← v.map_one]
case h
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
⊢ ↑v x < ↑v 1
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
⊢ ↑v (1 + x) = ↑v 1
apply map_add_eq_of_lt_left
no goals
case h
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
⊢ ↑v x < ↑v 1
simpa
no goals
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x < 1
this : ↑v' (1 + x) = 1
⊢ x = -1 + (1 + x)
simp
case mpr.h.mp.inr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v' x = 1
⊢ ↑v' x ≤ 1
case mpr.h.mp.inr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v x = 1
⊢ ↑v' x ≤ 1
rw [h] at hx'
no goals
case mpr.h.mp.inr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v x ≤ 1
hx' : ↑v' x = 1
⊢ ↑v' x ≤ 1
exact le_of_eq hx'
case mpr.h.mpr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
⊢ ↑v x ≤ 1
case mpr.h.mpr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
⊢ ↑v' x ≤ 1 → ↑v x ≤ 1
intro hx
case mpr.h.mpr.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
⊢ ↑v x ≤ 1

case mpr.h.mpr.inr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x = 1
⊢ ↑v x ≤ 1
case mpr.h.mpr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
⊢ ↑v x ≤ 1
cases' lt_or_eq_of_le hx with hx' hx'
case mpr.h.mpr.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
this : ↑v' (1 + x) = 1
⊢ ↑v x ≤ 1
case mpr.h.mpr.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
⊢ ↑v x ≤ 1
have : v' (1 + x) = 1 := by
  rw [← v'.map_one]
  apply map_add_eq_of_lt_left
  simpa
case mpr.h.mpr.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
this : ↑v (1 + x) = 1
⊢ ↑v x ≤ 1
case mpr.h.mpr.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
this : ↑v' (1 + x) = 1
⊢ ↑v x ≤ 1
rw [← h] at this
case mpr.h.mpr.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
this : ↑v (1 + x) = 1
⊢ ↑v (-1 + (1 + x)) ≤ 1
case mpr.h.mpr.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
this : ↑v (1 + x) = 1
⊢ ↑v x ≤ 1
rw [show x = -1 + (1 + x) by simp]
case mpr.h.mpr.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
this : ↑v (1 + x) = 1
⊢ max (↑v (-1)) (↑v (1 + x)) ≤ 1
case mpr.h.mpr.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
this : ↑v (1 + x) = 1
⊢ ↑v (-1 + (1 + x)) ≤ 1
refine' le_trans (v.map_add _ _) _
no goals
case mpr.h.mpr.inl
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
this : ↑v (1 + x) = 1
⊢ max (↑v (-1)) (↑v (1 + x)) ≤ 1
simp [this]
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
⊢ ↑v' (1 + x) = ↑v' 1
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
⊢ ↑v' (1 + x) = 1
rw [← v'.map_one]
case h
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
⊢ ↑v' x < ↑v' 1
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
⊢ ↑v' (1 + x) = ↑v' 1
apply map_add_eq_of_lt_left
no goals
case h
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
⊢ ↑v' x < ↑v' 1
simpa
no goals
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x < 1
this : ↑v (1 + x) = 1
⊢ x = -1 + (1 + x)
simp
case mpr.h.mpr.inr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v x = 1
⊢ ↑v x ≤ 1
case mpr.h.mpr.inr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v' x = 1
⊢ ↑v x ≤ 1
rw [← h] at hx'
no goals
case mpr.h.mpr.inr
K : Type u_3
F : Type ?u.3253919
R : Type ?u.3253922
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3253934
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
x : K
hx : ↑v' x ≤ 1
hx' : ↑v x = 1
⊢ ↑v x ≤ 1
exact le_of_eq hx'