K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
⊢ ↑v x ≤ ↑v y ↔ ↑v' x ≤ ↑v' y
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
⊢ IsEquiv v v'
intro x y
case pos
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : y = 0
⊢ ↑v x ≤ ↑v y ↔ ↑v' x ≤ ↑v' y

case neg
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v x ≤ ↑v y ↔ ↑v' x ≤ ↑v' y
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
⊢ ↑v x ≤ ↑v y ↔ ↑v' x ≤ ↑v' y
by_cases hy : y = 0
case neg
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v x ≤ ↑v (1 * y) ↔ ↑v' x ≤ ↑v' (1 * y)
case neg
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v x ≤ ↑v y ↔ ↑v' x ≤ ↑v' y
rw [show y = 1 * y by rw [one_mul]]
case neg
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v (x * y⁻¹ * y) ≤ ↑v (1 * y) ↔ ↑v' (x * y⁻¹ * y) ≤ ↑v' (1 * y)
case neg
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v x ≤ ↑v (1 * y) ↔ ↑v' x ≤ ↑v' (1 * y)
rw [← inv_mul_cancel_right₀ hy x]
case neg
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v (x * y⁻¹) * ↑v y ≤ ↑v 1 * ↑v y ↔ ↑v' (x * y⁻¹) * ↑v' y ≤ ↑v' 1 * ↑v' y
case neg
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v (x * y⁻¹ * y) ≤ ↑v (1 * y) ↔ ↑v' (x * y⁻¹ * y) ≤ ↑v' (1 * y)
iterate 2 rw [v.map_mul _ y, v'.map_mul _ y]
case neg
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y ↔ ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y
case neg
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v (x * y⁻¹) * ↑v y ≤ ↑v 1 * ↑v y ↔ ↑v' (x * y⁻¹) * ↑v' y ≤ ↑v' 1 * ↑v' y
rw [v.map_one, v'.map_one]
case neg.mp
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
H : ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y
⊢ ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y

case neg.mpr
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
H : ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y
⊢ ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y
case neg
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y ↔ ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y
constructor <;> intro H
no goals
case pos
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : y = 0
⊢ ↑v x ≤ ↑v y ↔ ↑v' x ≤ ↑v' y
simp [hy, zero_iff]
no goals
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ y = 1 * y
rw [one_mul]
case neg
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v (x * y⁻¹) * ↑v y ≤ ↑v 1 * ↑v y ↔ ↑v' (x * y⁻¹) * ↑v' y ≤ ↑v' 1 * ↑v' y
case neg
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
⊢ ↑v (x * y⁻¹) * ↑v y ≤ ↑v (1 * y) ↔ ↑v' (x * y⁻¹) * ↑v' y ≤ ↑v' (1 * y)
rw [v.map_mul _ y, v'.map_mul _ y]
case neg.mp.bc
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
H : ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y
⊢ ↑v' (x * y⁻¹) ≤ 1
case neg.mp
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
H : ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y
⊢ ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y
apply mul_le_mul_right'
case neg.mp.bc
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
H : ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y
hy : ↑v y ≠ 0
⊢ ↑v' (x * y⁻¹) ≤ 1
case neg.mp.bc
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
H : ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y
⊢ ↑v' (x * y⁻¹) ≤ 1
replace hy := v.ne_zero_iff.mpr hy
case neg.mp.bc
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ↑v y ≠ 0
H : ↑v (x * y⁻¹) ≤ 1
⊢ ↑v' (x * y⁻¹) ≤ 1
case neg.mp.bc
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
H : ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y
hy : ↑v y ≠ 0
⊢ ↑v' (x * y⁻¹) ≤ 1
replace H := le_of_le_mul_right hy H
no goals
case neg.mp.bc
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ↑v y ≠ 0
H : ↑v (x * y⁻¹) ≤ 1
⊢ ↑v' (x * y⁻¹) ≤ 1
rwa [h] at H
case neg.mpr.bc
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
H : ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y
⊢ ↑v (x * y⁻¹) ≤ 1
case neg.mpr
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
H : ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y
⊢ ↑v (x * y⁻¹) * ↑v y ≤ 1 * ↑v y
apply mul_le_mul_right'
case neg.mpr.bc
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
H : ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y
hy : ↑v' y ≠ 0
⊢ ↑v (x * y⁻¹) ≤ 1
case neg.mpr.bc
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ¬y = 0
H : ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y
⊢ ↑v (x * y⁻¹) ≤ 1
replace hy := v'.ne_zero_iff.mpr hy
case neg.mpr.bc
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ↑v' y ≠ 0
H : ↑v' (x * y⁻¹) ≤ 1
⊢ ↑v (x * y⁻¹) ≤ 1
case neg.mpr.bc
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
H : ↑v' (x * y⁻¹) * ↑v' y ≤ 1 * ↑v' y
hy : ↑v' y ≠ 0
⊢ ↑v (x * y⁻¹) ≤ 1
replace H := le_of_le_mul_right hy H
no goals
case neg.mpr.bc
K : Type u_3
F : Type ?u.3155721
R : Type ?u.3155724
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3155736
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
x y : K
hy : ↑v' y ≠ 0
H : ↑v' (x * y⁻¹) ≤ 1
⊢ ↑v (x * y⁻¹) ≤ 1
rwa [h]